Homotopy type theory and Voevodsky's univalent foundations
From MaRDI portal
Publication:2933829
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)
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.
Recommendations
Cites work
- scientific article; zbMATH DE number 2134022 (Why is no real title available?)
- scientific article; zbMATH DE number 3859117 (Why is no real title available?)
- scientific article; zbMATH DE number 3910392 (Why is no real title available?)
- scientific article; zbMATH DE number 29046 (Why is no real title available?)
- scientific article; zbMATH DE number 1302059 (Why is no real title available?)
- scientific article; zbMATH DE number 1302061 (Why is no real title available?)
- scientific article; zbMATH DE number 2079044 (Why is no real title available?)
- scientific article; zbMATH DE number 195199 (Why is no real title available?)
- scientific article; zbMATH DE number 937396 (Why is no real title available?)
- scientific article; zbMATH DE number 1420784 (Why is no real title available?)
- scientific article; zbMATH DE number 6296049 (Why is no real title available?)
- A formulation of the simple theory of types
- A history of algebraic and differential topology 1900--1960
- A model of type theory in simplicial sets. A brief introduction to Voevodsky's homotopy type theory
- A set of postulates for the foundation of logic. II
- A univalent formalization of the \(p\)-adic numbers
- Adjointness in foundations
- Algebraic classification of equivariant homotopy 2-types. I
- Algebraic operads
- An \(\omega\)-category with all duals is an \(\omega\)-groupoid
- Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
- Batanin higher groupoids and homotopy types
- Coherence for tricategories
- Combinatorial realizability models of type theory
- Computer theorem proving in mathematics
- Cosmoi of Internal Categories
- Formal proof
- Functionality in Combinatory Logic
- Group-like structures in general categories. I. Multiplications and comultiplications
- Higher Topos Theory (AM-170)
- Homologie singulière des espaces fibrés. Applications
- Homotopical algebra
- Homotopy theoretic models of identity types
- Homotopy type theory. Univalent foundations of mathematics
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Locally cartesian closed categories and type theory
- Martin-Löf complexes
- Monoidal globular categories as a natural environment for the theory of weak \(n\)-categories
- Nonstrict notions of \(n\)-category and \(n\)-groupoid via multisimplical sets
- On c.s.s. Complexes
- Spaces with finitely many non-trivial homotopy groups
- Symplectic theory of completely integrable Hamiltonian systems
- The Calculi of Lambda Conversion. (AM-6)
- The calculus of constructions
- The identity type weak factorisation system
- The strict \(\omega\)-groupoid interpretation of type theory
- Topology and groupoids
- Type theory and homotopy
- Types and programing languages
- Types are weak \(\omega \)-groupoids
- Voevodsky’s Univalence Axiom in Homotopy Type Theory
- Weak omega-categories from intensional type theory
- Zur Deutung der intuitionistischen Logik
Cited in
(42)- Observability in the univalent universe
- An introduction to univalent foundations for mathematicians
- On the ∞$\infty$‐topos semantics of homotopy type theory
- Mathesis Universalis and Homotopy Type Theory
- Homotopy Type Theory: A synthetic approach to higher equalities
- The Seifert-van Kampen Theorem in Homotopy Type Theory
- Univalent foundations of mathematics
- Formal universes
- Categorical structures for type theory in univalent foundations
- Mini-workshop: The homotopy interpretation of constructive type theory. Abstracts from the mini-workshop held February 27th-March 05th, 2011.
- Martin Hofmann’s contributions to type theory: Groupoids and univalence
- Topological model of neural information networks
- Introduction -- from type theory and homotopy theory to univalent foundations
- The homotopy theory of type theories
- Type theory and homotopy
- Homotopy type theory in Lean
- \(\pi _{n }(S ^{n })\) in homotopy type theory
- Lawvere-Tierney sheafification in Homotopy Type Theory
- A meaning explanation for HoTT
- Higher Structures in Homotopy Type Theory
- Preface: Special issue on homotopy type theory and univalent foundations
- scientific article; zbMATH DE number 7204300 (Why is no real title available?)
- Higher inductive types as homotopy-initial algebras
- Homotopy limits in type theory
- Homotopy type theory
- Homotopy type theory and the formalization of mathematics
- A univalent formalization of the \(p\)-adic numbers
- Brouwer's fixed-point theorem in real-cohesive 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
- scientific article; zbMATH DE number 1420784 (Why is no real title available?)
- Non-wellfounded trees in homotopy type theory
- Cubical methods in homotopy type theory and univalent foundations
- Der Code der Mathematik
- Homotopy type theory. Univalent foundations of mathematics
- Proof and computation II. From proof theory and univalent mathematics to program extraction and verification. Based on the international autumn school ``Proof and computation, September 20--26, 2019
- Wild \(\omega\)-categories for the homotopy hypothesis in type theory
- Homotopy type theory: the logic of space
- Preface to the MSCS Issue 31.1 (2021) Homotopy type theory and univalent foundations. II
- The simplicial model of univalent foundations (after Voevodsky)
- An experimental library of formalized mathematics based on the univalent foundations
- Towards a constructive simplicial model of Univalent Foundations
- Idempotents in intensional type theory
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)
