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

DOI10.1017/S0960129521000098MaRDI QIDQ5076386zbMATH OpenOpenAlexFDO

Authors 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

Categorical semanticscoherencedependent type theory

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 2079044
• Functional completeness of the free locally Cartesian closed category and interpretations of Martin-Löf's theory of dependent types
• Revisiting the categorical interpretation of dependent type theory
• The interpretation of intuitionistic type theory in locally Cartesian closed categories -- an intuitionistic perspective
• The local universes model: an overlooked coherence construction for dependent type theories

Cites work

• Algebraic models for higher categories
• Coalgebraic models for combinatorial model categories
• Enriched model categories and presheaf categories
• Equipping weak equivalences with algebraic structure
• Fibrations and geometric realizations
• Higher Topos Theory (AM-170)
• Homotopy-theoretic aspects of 2-monads
• scientific article; zbMATH DE number 4177054 (Why is no real title available?)
• scientific article; zbMATH DE number 5695342 (Why is no real title available?)
• scientific article; zbMATH DE number 3751225 (Why is no real title available?)
• scientific article; zbMATH DE number 2079044 (Why is no real title available?)
• scientific article; zbMATH DE number 1860105 (Why is no real title available?)
• Internal type theory
• Kan extensions in enriched category theory
• Locally cartesian closed categories and type theory
• Sketches for arithmetic universes
• The biequivalence of locally Cartesian closed categories and Martin-Löf type theories
• The local universes model: an overlooked coherence construction for dependent type theories
• Two-dimensional monad theory

Cited in

(2)

• Modular correspondence between dependent type theories and categories including pretopoi and topoi
• scientific article; zbMATH DE number 2079044 (Why is no real title available?)

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5076386)