Modeling Martin-Löf type theory in categories

DOI10.1016/J.JAL.2013.08.003MaRDI QIDQ280835zbMATH OpenOpenAlexFDO

Authors François Lamarche

Publication date 10 May 2016

Published in Journal of Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.jal.2013.08.003

zbMATH Keywords

Grothendieck fibrationhomotopical type theoryidentity typepath objectMartin-Löf type theory

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Topological categories, foundations of homotopy theory (55U40) Fibered categories (18D30)

Recommendations

• Topological and simplicial models of identity types
• Homotopy-theoretic models of type theory
• Model structures on categories of models of type theories
• Homotopy theoretic models of identity types
• On a model invariance problem in homotopy type theory

Cites work

• scientific article; zbMATH DE number 1302059 (Why is no real title available?)
• scientific article; zbMATH DE number 2079044 (Why is no real title available?)
• scientific article; zbMATH DE number 786486 (Why is no real title available?)
• A model of type theory in simplicial sets. A brief introduction to Voevodsky's homotopy type theory
• Categorical logic and type theory
• Generalized algebraic theories and contextual categories
• Handbook of logic in computer science. Vol. 5: Logical and algebraic methods
• Homotopy theoretic models of identity types
• Metric spaces, generalized logic, and closed categories
• The identity type weak factorisation system
• Topological and simplicial models of identity types
• Types are weak \(\omega \)-groupoids

Cited in

(7)

• Martin-Löf identity types in C-systems
• MODELS OF MARTIN-LÖF TYPE THEORY FROM ALGEBRAIC WEAK FACTORISATION SYSTEMS
• Identity types and weak factorization systems in Cauchy complete categories
• Path categories and propositional identity types
• Towards formalizing categorical models of type theory in type theory
• Topological and simplicial models of identity types
• On a model invariance problem in homotopy type theory

This page was built for publication: Modeling Martin-Löf type theory in categories

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