Homotopy type theory
From MaRDI portal
Categorical logic, topoi (03G30) Foundations, relations to logic and deductive systems (18A15) Categories of sets, characterizations (18B05) Abstract and axiomatic homotopy theory in algebraic topology (55U35) Topological categories, foundations of homotopy theory (55U40) Functional programming and lambda calculus (68N18)
Recommendations
Cited in
(41)- The homotopy theory of type theories
- Univalence as a principle of logic
- The simplicial model of univalent foundations (after Voevodsky)
- Type theory and formalisation of mathematics
- Observability in the univalent universe
- A model of type theory in simplicial sets. A brief introduction to Voevodsky's homotopy type theory
- Higher inductive types as homotopy-initial algebras
- Homotopy type theory and Voevodsky's univalent foundations
- Homotopy Type Theory
- \(\pi _{n }(S ^{n })\) in homotopy type theory
- Theory of dependent types and axiom of univalence
- Homotopy type theory and the formalization of mathematics
- Univalent semantics of constructive type theories
- Mathesis Universalis and Homotopy Type Theory
- Pro-algebraic homotopy types
- Brouwer's fixed-point theorem in real-cohesive homotopy type theory
- An introduction to univalent foundations for mathematicians
- scientific article; zbMATH DE number 877845 (Why is no real title available?)
- scientific article; zbMATH DE number 1420784 (Why is no real title available?)
- Quantum gauge field theory in cohesive homotopy type theory
- Preface to the MSCS Issue 31.1 (2021) Homotopy type theory and univalent foundations. II
- Homotopy Type Theory: A synthetic approach to higher equalities
- Synthetic topology in Homotopy Type Theory for probabilistic programming
- Cellular Cohomology in Homotopy Type Theory
- Preface to the MSCS Issue 31.1 (2021) Homotopy type theory and univalent foundations
- Lawvere-Tierney sheafification in Homotopy Type Theory
- Modalities in homotopy type theory
- Venus homotopically
- Localization in Homotopy Type Theory
- Identity in homotopy type theory. II: The conceptual and philosophical status of identity in HoTT
- UNIVERSES AND UNIVALENCE IN HOMOTOPY TYPE THEORY
- Univalent foundations of mathematics and paraconsistency
- Type theory and homotopy
- The Seifert-van Kampen Theorem in Homotopy Type Theory
- Homotopy type theory. Univalent foundations of mathematics
- Towards Constructive Homological Algebra in Type Theory
- Introduction -- from type theory and homotopy theory to univalent foundations
- Univalence for inverse diagrams and homotopy canonicity
- The univalence axiom for elegant Reedy presheaves
- Decomposing the univalence axiom
- The p-adic Jaynes-Cummings model in symplectic geometry
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 Q2969774)
