Homotopy Type Theory

DOI10.1007/978-3-662-45824-2_1MaRDI QIDQ2937385zbMATH OpenOpenAlexFDO

Authors Steve Awodey

Publication date 9 January 2015

Published in Logic and Its Applications (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-662-45824-2_1

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Categorical logic, topoi (03G30) Topological categories, foundations of homotopy theory (55U40)

Recommendations

• Homotopy type theory
• Type theory and homotopy
• The homotopy theory of type theories
• Homotopy type theory and the formalization of mathematics
• Higher Structures in Homotopy Type Theory
• Homotopy-theoretic models of type theory
• Homotopy type theory. Univalent foundations of mathematics
• Homotopy Type Theory in Isabelle
• scientific article; zbMATH DE number 937396
• Homotopy-initial algebras in type theory

Cited in

(40)

• The homotopy theory of type theories
• The Frobenius condition, right properness, and uniform fibrations
• A meaning explanation for HoTT
• Expressing `the structure of' in homotopy type theory
• Type theory and formalisation of mathematics
• A model of type theory in simplicial sets. A brief introduction to Voevodsky's homotopy type theory
• Homotopical patch theory
• Homotopy type theory and Voevodsky's univalent foundations
• \(\pi _{n }(S ^{n })\) in homotopy type theory
• Identity in homotopy type theory. Part I: The justification of path induction
• Theory of dependent types and axiom of univalence
• Homotopy type theory
• Inductive types in homotopy type theory
• Homotopy type theory and the formalization of mathematics
• Univalent foundations of mathematics
• Univalent semantics of constructive type theories
• Mathesis Universalis and Homotopy Type Theory
• Mini-workshop: The homotopy interpretation of constructive type theory. Abstracts from the mini-workshop held February 27th-March 05th, 2011.
• Does homotopy type theory provide a foundation for mathematics?
• scientific article; zbMATH DE number 877845 (Why is no real title available?)
• Quantum gauge field theory in cohesive homotopy type theory
• Homotopy Type Theory: A synthetic approach to higher equalities
• Synthetic topology in Homotopy Type Theory for probabilistic programming
• A cubical language for Bishop sets
• What types should not be
• Cellular Cohomology in Homotopy Type Theory
• Preface to the MSCS Issue 31.1 (2021) Homotopy type theory and univalent foundations
• Homotopy type theory: the logic of space
• Lawvere-Tierney sheafification in Homotopy Type Theory
• Modalities in homotopy type theory
• Modal Homotopy Type Theory
• Localization in Homotopy Type Theory
• Type theory and homotopy
• The Seifert-van Kampen Theorem in Homotopy Type Theory
• Towards Constructive Homological Algebra in Type Theory
• Introduction -- from type theory and homotopy theory to univalent foundations
• An experimental library of formalized mathematics based on the univalent foundations
• Naïve Type Theory
• The compatibility of the minimalist foundation with homotopy type theory
• Extended abstracts fall 2013. Geometrical analysis; type theory, homotopy theory and univalent foundations. Selected papers based on the presentations at the conferences, CRM, Barcelona, Spain, July 1--5, 2013 and September 23--27, 2013

This page was built for publication: Homotopy Type Theory

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