Introduction – from type theory and homotopy theory to univalent foundations

DOI10.1017/S0960129514000474zbMath1362.03004DBLPjournals/mscs/AwodeyGP15OpenAlexW2043828421WikidataQ59897037 ScholiaQ59897037MaRDI QIDQ5740647

No author found.

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/s0960129514000474

Mathematics Subject Classification ID

Collections of articles of miscellaneous specific interest (00B15) Categorical logic, topoi (03G30) Proceedings, conferences, collections, etc. pertaining to mathematical logic and foundations (03-06) Topological categories, foundations of homotopy theory (55U40) Foundations, relations to logic and deductive systems (18A15)

Cites Work

• Homotopical algebraic geometry. I: Topos theory
• The identity type weak factorisation system
• Homotopical algebra
• Types are weak ω -groupoids
• Homotopy theoretic models of identity types
• A model for the homotopy theory of homotopy theory
• Homotopy Type Theory: Univalent Foundations of Mathematics

This page was built for publication: Introduction – from type theory and homotopy theory to univalent foundations