Modeling Martin-Löf type theory in categories

DOI10.1016/J.JAL.2013.08.003zbMath1335.03009OpenAlexW1971619141MaRDI QIDQ280835

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

Martin-Löf type theoryGrothendieck fibrationhomotopical type theoryidentity typepath object

Mathematics Subject Classification ID

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A model of type theory in simplicial sets. A brief introduction to Voevodsky's homotopy type theory
• The identity type weak factorisation system
• Generalized algebraic theories and contextual categories
• Categorical logic and type theory
• Topological and Simplicial Models of Identity Types
• Types are weak ω -groupoids
• Homotopy theoretic models of identity types
• Metric spaces, generalized logic, and closed categories

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