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

DOI10.1016/J.JAL.2013.04.001MaRDI QIDQ280837zbMATH OpenOpenAlexFDO

Authors 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

type theoryhomotopy theorycategorical modelsunivalence axiom

Mathematics Subject Classification ID

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

Recommendations

• The simplicial model of univalent foundations (after Voevodsky)
• Homotopy Type Theory
• Homotopy type theory
• W-types in homotopy type theory
• Homotopy theoretic models of identity types

Cites work

• scientific article; zbMATH DE number 1241699 (Why is no real title available?)
• scientific article; zbMATH DE number 1302059 (Why is no real title available?)
• scientific article; zbMATH DE number 226803 (Why is no real title available?)
• Homotopy theoretic models of identity types
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Simplicial homotopy theory

Cited in

(24)

• On the ∞$\infty$‐topos semantics of homotopy type theory
• Univalence in locally Cartesian closed categories
• W-types in homotopy type theory
• Two-sided Cartesian fibrations of synthetic \((\infty, 1)\)-categories
• The law of excluded middle in the simplicial model of type theory
• Homotopy type theory and Voevodsky's univalent foundations
• Internal sums for synthetic fibered \((\infty,1)\)-categories
• Extending homotopy type theory with strict equality
• \(\pi _{n }(S ^{n })\) in homotopy type theory
• Homotopy theoretic models of identity types
• Axioms for modelling cubical type theory in a topos
• From multisets to sets in homotopy type theory
• The strict \(\omega\)-groupoid interpretation of type theory
• Sets in homotopy type theory
• Simplicial sets inside cubical sets
• A dependently-typed construction of semi-simplicial types
• A syntactical approach to weak omega-groupoids
• The simplicial model of univalent foundations (after Voevodsky)
• A generalization of the Takeuti-Gandy interpretation
• Modeling Martin-Löf type theory in categories
• scientific article; zbMATH DE number 7566056 (Why is no real title available?)
• Towards a constructive simplicial model of Univalent Foundations
• Homotopy-theoretic models of type theory
• Univalent semantics of constructive type theories

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

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