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

DOI10.1016/J.JAL.2013.04.001zbMATH Open1335.03010OpenAlexW200058515MaRDI QIDQ280837FDOQ280837

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

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

zbMATH Keywords

type theoryhomotopy theorycategorical modelsunivalence axiom

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• Simplicial homotopy theory
• Homotopy theoretic models of identity types
• Title not available (Why is that?)
• Title not available (Why is that?)
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.

Cited In (10)

• On the ∞$\infty$‐topos semantics of homotopy type theory
• Univalence in locally Cartesian closed categories
• Two-sided Cartesian fibrations of synthetic \((\infty, 1)\)-categories
• Homotopy type theory and Voevodsky’s univalent foundations
• Modeling Martin-Löf type theory in categories
• Simplicial sets inside cubical sets
• Towards a constructive simplicial model of Univalent Foundations
• Internal sums for synthetic fibered \((\infty,1)\)-categories
• Title not available (Why is that?)
• Homotopy theoretic models of identity types

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)