Modeling Martin-Löf type theory in categories
From MaRDI portal
Publication:280835
DOI10.1016/J.JAL.2013.08.003zbMATH Open1335.03009OpenAlexW1971619141MaRDI QIDQ280835FDOQ280835
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
Recommendations
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 \(\omega \)-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 (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)
