Two-dimensional models of type theory

Richard Garner*

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

25 Citations (Scopus)
14 Downloads (Pure)


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.

Original languageEnglish
Pages (from-to)687-736
Number of pages50
JournalMathematical Structures in Computer Science
Issue number4
Publication statusPublished - Aug 2009
Externally publishedYes

Bibliographical 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


Dive into the research topics of 'Two-dimensional models of type theory'. Together they form a unique fingerprint.

Cite this