Modeling Martin-Löf type theory in categories

DOI10.1016/J.JAL.2013.08.003zbMATH Open1335.03009OpenAlexW1971619141MaRDI QIDQ280835FDOQ280835

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

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

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)

Cites Work

• Categorical logic and type theory
• Handbook of logic in computer science. Vol. 5: Logical and algebraic methods
• Metric spaces, generalized logic, and closed categories
• Generalized algebraic theories and contextual categories
• A model of type theory in simplicial sets. A brief introduction to Voevodsky's homotopy type theory
• Topological and Simplicial Models of Identity Types
• Types are weak ω -groupoids
• Homotopy theoretic models of identity types
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• The identity type weak factorisation system

Cited In (1)

• Martin-Löf identity types in C-systems

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)