Two-dimensional models of type theory

DOI10.1017/S0960129509007646zbMath1230.03043arXiv0808.2122OpenAlexW2170599098MaRDI QIDQ3395310

Richard Garner

Publication date: 26 August 2009

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/0808.2122

zbMATH Keywords

Martin-Löf type theorycategorical semantics

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Categorical semantics of formal languages (18C50)

Related Items

Homotopical patch theory ⋮ Data Types with Symmetries and Polynomial Functors over Groupoids ⋮ Proof-Relevant Parametricity ⋮ Unnamed Item ⋮ Martin-Löf complexes ⋮ Internal languages of finitely complete \((\infty , 1)\)-categories ⋮ Bicategorical type theory: semantics and syntax ⋮ Accessible aspects of 2-category theory ⋮ Homotopical inverse diagrams in categories with attributes ⋮ 2-Dimensional Directed Type Theory ⋮ The homotopy theory of type theories ⋮ On the strength of dependent products in the type theory of Martin-Löf ⋮ Type Theory and Homotopy

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Telescopic mappings in typed lambda calculus
• The identity type weak factorisation system
• On the strength of dependent products in the type theory of Martin-Löf
• Generalized algebraic theories and contextual categories
• Comprehension categories and the semantics of type dependency
• Constructions of factorization systems in categories
• Categorical logic and type theory
• Some properties of Fib as a fibred \(2\)-category
• Locally cartesian closed categories and type theory
• Homotopy limits for 2-categories
• Homotopy theoretic models of identity types
• Elementary observations on 2-categorical limits
• Some algebraic problems in the context of functorial semantics of algebraic theories

This page was built for publication: Two-dimensional models of type theory