A dependently-typed construction of semi-simplicial types

DOI10.1017/S0960129514000528zbMATH Open1362.03006OpenAlexW2064744640MaRDI QIDQ5740652FDOQ5740652

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

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

Mathematics Subject Classification ID

Categorical logic, topoi (03G30)

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)