Two-dimensional models of type theory

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.

46 pages; v2: final journal version

References in corpus (3)

• Homotopy theoretic models of identity types
• The identity type weak factorisation system
• On the strength of dependent products in the type theory of Martin-Löf

Cited by in corpus (13)

• The identity type weak factorisation system
• Weak omega-categories from intensional type theory
• On the strength of dependent products in the type theory of Martin-Löf
• Type theory and homotopy
• The homotopy theory of type theories
• Homotopy Theoretic Models of Type Theory
• Accessible aspects of 2-category theory
• Signatures and Induction Principles for Higher Inductive-Inductive Types
• Bicategorical type theory: semantics and syntax
• Homotopical inverse diagrams in categories with attributes
• Coherence of strict equalities in dependent type theories
• A category-theoretic version of the identity type weak factorization system
• On $2$-categorical $\infty$-cosmoi