@article{05c0f2868a6645be807c18ae0849b679,
title = "Two-dimensional models of type theory",
abstract = "We describe a non-extensional variant of Martin-Lf type theory, which we call two-dimensional type theory, and equip it with a sound and complete semantics valued in 2-categories.",
author = "Richard Garner",
note = "Copyright [2009] Cambridge University Press. Article originally published in [Garner R. {"}Two-dimensional models of type theory{"}. Mathematical Structures in Computer Science, 19:4,687- 736]. The original article can be found at http://dx.doi.org/10.1017/S0960129509007646.",
year = "2009",
month = aug,
doi = "10.1017/S0960129509007646",
language = "English",
volume = "19",
pages = "687--736",
journal = "Mathematical Structures in Computer Science",
issn = "0960-1295",
publisher = "Cambridge University Press (CUP)",
number = "4",
}