Homotopy type theory and Voevodsky's univalent foundations
From MaRDI portal
Publication:2933829
DOI10.1090/S0273-0979-2014-01456-9zbMATH Open1432.03019arXiv1210.5658OpenAlexW2962780223MaRDI QIDQ2933829FDOQ2933829
Michael A. Warren, Álvaro Pelayo
Publication date: 8 December 2014
Published in: Bulletin of the American Mathematical Society (Search for Journal in Brave)
Abstract: Recent discoveries have been made connecting abstract homotopy theory and the field of type theory from logic and theoretical computer science. This has given rise to a new field, which has been christened "homotopy type theory". In this direction, Vladimir Voevodsky observed that it is possible to model type theory using simplicial sets and that this model satisfies an additional property, called the Univalence Axiom, which has a number of striking consequences. He has subsequently advocated a program, which he calls univalent foundations, of developing mathematics in the setting of type theory with the Univalence Axiom and possibly other additional axioms motivated by the simplicial set model. Because type theory possesses good computational properties, this program can be carried out in a computer proof assistant. In this paper we give an introduction to homotopy type theory in Voevodsky's setting, paying attention to both theoretical and practical issues. In particular, the paper serves as an introduction to both the general ideas of homotopy type theory as well as to some of the concrete details of Voevodsky's work using the well-known proof assistant Coq. The paper is written for a general audience of mathematicians with basic knowledge of algebraic topology; the paper does not assume any preliminary knowledge of type theory, logic, or computer science.
Full work available at URL: https://arxiv.org/abs/1210.5658
Recommendations
Categorical logic, topoi (03G30) Abstract and axiomatic homotopy theory in algebraic topology (55U35) Topological categories, foundations of homotopy theory (55U40) Functional programming and lambda calculus (68N18) Type theory (03B38) Categories of fibrations, relations to (K)-theory, relations to type theory (18N45)
Cites Work
- Title not available (Why is that?)
- Algebraic Operads
- Homotopical algebra
- Title not available (Why is that?)
- Title not available (Why is that?)
- Higher Topos Theory (AM-170)
- Title not available (Why is that?)
- Group-like structures in general categories. I. Multiplications and comultiplications
- Monoidal globular categories as a natural environment for the theory of weak \(n\)-categories
- A model of type theory in simplicial sets. A brief introduction to Voevodsky's homotopy type theory
- Types are weak ω -groupoids
- Title not available (Why is that?)
- Homotopy theoretic models of identity types
- Title not available (Why is that?)
- Title not available (Why is that?)
- Homotopy Type Theory: Univalent Foundations of Mathematics
- A formulation of the simple theory of types
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- The identity type weak factorisation system
- Homologie singulière des espaces fibrés. Applications
- Spaces with finitely many non-trivial homotopy groups
- Locally cartesian closed categories and type theory
- Title not available (Why is that?)
- Zur Deutung der intuitionistischen Logik
- Types and programing languages
- Symplectic theory of completely integrable Hamiltonian systems
- Coherence for tricategories
- The calculus of constructions
- Topology and groupoids
- Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
- Weak omega-categories from intensional type theory
- Martin-Löf complexes
- Combinatorial realizability models of type theory
- Title not available (Why is that?)
- Type Theory and Homotopy
- Title not available (Why is that?)
- On c.s.s. Complexes
- Title not available (Why is that?)
- Batanin higher groupoids and homotopy types
- Title not available (Why is that?)
- Nonstrict notions of \(n\)-category and \(n\)-groupoid via multisimplical sets
- Algebraic classification of equivariant homotopy 2-types. I
- A set of postulates for the foundation of logic. II
- The Calculi of Lambda Conversion. (AM-6)
- Functionality in Combinatory Logic
- Computer theorem proving in mathematics
- Adjointness in foundations
- Cosmoi of Internal Categories
- A history of algebraic and differential topology 1900--1960
- An \(\omega\)-category with all duals is an \(\omega\)-groupoid
- Title not available (Why is that?)
- Voevodsky’s Univalence Axiom in Homotopy Type Theory
- A univalent formalization of the p-adic numbers
Cited In (19)
- The homotopy theory of type theories
- The Seifert-van Kampen Theorem in Homotopy Type Theory
- Title not available (Why is that?)
- On the ∞$\infty$‐topos semantics of homotopy type theory
- Martin Hofmann’s contributions to type theory: Groupoids and univalence
- Topological model of neural information networks
- The simplicial model of univalent foundations (after Voevodsky)
- Mathesis Universalis and Homotopy Type Theory
- Formal Universes
- Homotopy Type Theory: A synthetic approach to higher equalities
- Higher inductive types as homotopy-initial algebras
- Cubical methods in homotopy type theory and univalent foundations
- Idempotents in intensional type theory
- A meaning explanation for HoTT
- Categorical structures for type theory in univalent foundations
- A univalent formalization of the p-adic numbers
- Title not available (Why is that?)
- Lawvere-Tierney sheafification in Homotopy Type Theory
- Observability in the univalent universe
Uses Software
This page was built for publication: Homotopy type theory and Voevodsky's univalent foundations
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2933829)
