Models of Type Theory Based on Moore Paths

DOI10.4230/LIPICS.FSCD.2017.28zbMATH Open1434.03043OpenAlexW3021153996MaRDI QIDQ5111326FDOQ5111326

Ian Orton, Andrew M. Pitts

Publication date: 26 May 2020

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

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

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)

Cites Work

• Sheaves in geometry and logic: a first introduction to topos theory
• Title not available (Why is that?)
• Title not available (Why is that?)
• Topological and Simplicial Models of Identity Types
• Title not available (Why is that?)
• Homotopy Type Theory: Univalent Foundations of Mathematics
• On a Topological Topos
• Internal type theory
• Title not available (Why is that?)
• A combinatorial definition of homotopy groups
• Modular correspondence between dependent type theories and categories including pretopoi and topoi
• Wellfounded trees in categories
• Title not available (Why is that?)
• The simplicial model of univalent foundations (after Voevodsky)
• The Local Universes Model
• Title not available (Why is that?)
• Cubical Type Theory: a constructive interpretation of the univalence axiom
• Title not available (Why is that?)
• Title not available (Why is that?)
• Globalizing fibrations by schedules

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)