Models of Type Theory Based on Moore Paths

DOI10.4230/LIPICS.FSCD.2017.28MaRDI QIDQ5111326zbMATH OpenOpenAlexFDO

Authors Ian Orton, Andrew M. Pitts

Publication date 26 May 2020

Full work available at URL https://doi.org/10.4230/LIPIcs.FSCD.2017.28

zbMATH Keywords

toposhomotopy theorydependent type theoryMoore path

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Abstract and axiomatic homotopy theory in algebraic topology (55U35) Type theory (03B38)

Recommendations

• Models of type theory based on Moore paths
• Topological and simplicial models of identity types
• Homotopy-theoretic models of type theory
• Homotopy theoretic models of identity types
• scientific article; zbMATH DE number 7003193

Cites work

• scientific article; zbMATH DE number 6694181 (Why is no real title available?)
• scientific article; zbMATH DE number 3785000 (Why is no real title available?)
• scientific article; zbMATH DE number 29046 (Why is no real title available?)
• scientific article; zbMATH DE number 3521950 (Why is no real title available?)
• scientific article; zbMATH DE number 1241699 (Why is no real title available?)
• scientific article; zbMATH DE number 2247252 (Why is no real title available?)
• A combinatorial definition of homotopy groups
• Axioms for modelling cubical type theory in a topos
• Cubical type theory: a constructive interpretation of the univalence axiom
• Globalizing fibrations by schedules
• Homotopy type theory. Univalent foundations of mathematics
• Internal type theory
• Modular correspondence between dependent type theories and categories including pretopoi and topoi
• On a Topological Topos
• Sheaves in geometry and logic: a first introduction to topos theory
• Stack semantics of type theory
• The local universes model: an overlooked coherence construction for dependent type theories
• The simplicial model of univalent foundations (after Voevodsky)
• Topological and simplicial models of identity types
• Wellfounded trees in categories

Cited in

(2)

• Models of type theory based on Moore paths
• Combinatorial realizability models of type theory

Describes a project that uses

Uses Software

• cubicaltt

This page was built for publication: Models of Type Theory Based on Moore Paths

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