A dependently-typed construction of semi-simplicial types

DOI10.1017/S0960129514000528MaRDI QIDQ5740652zbMATHOpenAlexFDO

Authors Hugo Herbelin

Publication date 27 July 2016

Published in Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1017/s0960129514000528

Mathematics Subject Classification ID

Categorical logic, topoi (03G30)

Recommendations

• The simplicial model of univalent foundations (after Voevodsky)
• A model of type theory in simplicial sets. A brief introduction to Voevodsky's homotopy type theory
• Univalent semantics of constructive type theories
• A generalization of the Takeuti-Gandy interpretation
• Cubical type theory: a constructive interpretation of the univalence axiom

Cites work

• Survey article: an elementary illustrated introduction to simplicial sets

Cited in

(2)

• Functional Kan simplicial sets: non-constructivity of exponentiation
• A rewriting coherence theorem with applications in homotopy type theory

This page was built for publication: A dependently-typed construction of semi-simplicial types

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