Two-dimensional models of type theory
From MaRDI portal
Abstract: We describe a non-extensional variant of Martin-L"of type theory which we call two-dimensional type theory, and equip it with a sound and complete semantics valued in 2-categories.
Recommendations
Cites work
- Categorical logic and type theory
- Comprehension categories and the semantics of type dependency
- Constructions of factorization systems in categories
- Elementary observations on 2-categorical limits
- Generalized algebraic theories and contextual categories
- Homotopy limits for 2-categories
- Homotopy theoretic models of identity types
- scientific article; zbMATH DE number 3751225 (Why is no real title available?)
- scientific article; zbMATH DE number 50149 (Why is no real title available?)
- scientific article; zbMATH DE number 1289305 (Why is no real title available?)
- Locally cartesian closed categories and type theory
- On the strength of dependent products in the type theory of Martin-Löf
- Some algebraic problems in the context of functorial semantics of algebraic theories
- Some properties of Fib as a fibred \(2\)-category
- Telescopic mappings in typed lambda calculus
- The identity type weak factorisation system
Cited in
(21)- On the strength of dependent products in the type theory of Martin-Löf
- Two-dimensional monad theory
- Type 2 representation and reasoning for CWW
- The homotopy theory of type theories
- Accessible aspects of 2-category theory
- Homotopical inverse diagrams in categories with attributes
- Internal languages of finitely complete ( , 1)-categories
- Canonicity for 2-dimensional type theory
- Data types with symmetries and polynomial functors over groupoids
- Proof-Relevant Parametricity
- Martin-Löf complexes
- An Ad-Hoc Semantics to Study Structural Properties of Types
- Signatures and induction principles for higher inductive-inductive types
- Type theory and homotopy
- Homotopical patch theory
- 2-Dimensional Directed Type Theory
- Bicategorical type theory: semantics and syntax
- Semantics for two-dimensional type theory
- Relating homotopy equivalences to conservativity in dependent type theories with computation axioms
- Extensional concepts in intensional type theory, revisited
- A 2-categorical approach to the semantics of dependent type theory with computation axioms
This page was built for publication: Two-dimensional models of type theory
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3395310)
