Two-dimensional models of type theory
Logic
2011-10-17 v2 Category Theory
Abstract
We describe a non-extensional variant of Martin-L\"of type theory which we call two-dimensional type theory, and equip it with a sound and complete semantics valued in 2-categories.
Cite
@article{arxiv.0808.2122,
title = {Two-dimensional models of type theory},
author = {Richard Garner},
journal= {arXiv preprint arXiv:0808.2122},
year = {2011}
}
Comments
46 pages; v2: final journal version