Misc,

Two-dimensional models of type theory

.
(2008)cite http://arxiv.org/abs/0808.2122arxiv:0808.2122Comment: 46 pages; v2: final journal version.
DOI: 10.1017/S0960129509007646

Abstract

We describe a non-extensional variant of Martin-Löf type theory which we call two-dimensional type theory, and equip it with a sound and complete semantics valued in 2-categories.

Tags

Users

  • @t.uemura

Comments and Reviews