Modeling Martin-Löf type theory in categories
From MaRDI portal
Publication:280835
DOI10.1016/J.JAL.2013.08.003zbMath1335.03009OpenAlexW1971619141MaRDI QIDQ280835
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
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