Two-dimensional models of type theory

Richard Garner*

*Corresponding author for this work

Research output: Contribution to journalArticle

21 Citations (Scopus)
3 Downloads (Pure)

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.

Original languageEnglish
Pages (from-to)687-736
Number of pages50
JournalMathematical Structures in Computer Science
Volume19
Issue number4
DOIs
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 http://dx.doi.org/10.1017/S0960129509007646.

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

  • Cite this