A model of type theory in simplicial sets. A brief introduction to Voevodsky's homotopy type theory

DOI10.1016/j.jal.2013.04.001zbMath1335.03010OpenAlexW200058515MaRDI QIDQ280837

Thomas Streicher

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.04.001

zbMATH Keywords

categorical modelstype theoryhomotopy theoryunivalence axiom

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Topological categories, foundations of homotopy theory (55U40)

Related Items (6)

Modeling Martin-Löf type theory in categories ⋮ Homotopy type theory and Voevodsky’s univalent foundations ⋮ On the ∞$\infty$‐topos semantics of homotopy type theory ⋮ Towards a constructive simplicial model of Univalent Foundations ⋮ Univalence in locally Cartesian closed categories ⋮ Unnamed Item

Cites Work

• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Homotopy theoretic models of identity types
• Simplicial homotopy theory
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A model of type theory in simplicial sets. A brief introduction to Voevodsky's homotopy type theory