An interpretation of dependent type theory in a model category of locally cartesian closed categories

DOI10.1017/S0960129521000098OpenAlexW3199901623MaRDI QIDQ5076386

Martin E. Bidlingmaier

Publication date: 17 May 2022

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

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

zbMATH Keywords

coherencedependent type theoryCategorical semantics

Mathematics Subject Classification ID

Type theory (03B38) Categories of fibrations, relations to (K)-theory, relations to type theory (18N45)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Algebraic models for higher categories
• Homotopy-theoretic aspects of 2-monads
• Two-dimensional monad theory
• Coalgebraic models for combinatorial model categories
• Enriched model categories and presheaf categories
• Equipping weak equivalences with algebraic structure
• Kan extensions in enriched category theory
• The Local Universes Model
• The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories
• Locally cartesian closed categories and type theory
• Fibrations and geometric realizations
• Internal type theory
• Sketches for arithmetic universes
• Higher Topos Theory (AM-170)

This page was built for publication: An interpretation of dependent type theory in a model category of locally cartesian closed categories