Homotopy type theory and Voevodsky's univalent foundations
From MaRDI portal
(Redirected from 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 -groupoids
- Voevodsky’s Univalence Axiom in Homotopy Type Theory
- Weak omega-categories from intensional type theory
- Zur Deutung der intuitionistischen Logik
Cited in
(43)- Lawvere-Tierney sheafification in Homotopy Type Theory
- Observability in the univalent universe
- Preface: Special issue on homotopy type theory and univalent foundations
- The homotopy theory of type theories
- Homotopy limits in type theory
- \(\pi _{n }(S ^{n })\) in homotopy type theory
- The Seifert-van Kampen Theorem in Homotopy Type Theory
- A univalent formalization of the \(p\)-adic numbers
- scientific article; zbMATH DE number 1420784 (Why is no real title available?)
- Formal universes
- Topological model of neural information networks
- The p-adic Jaynes-Cummings model in symplectic geometry
- Martin Hofmann’s contributions to type theory: Groupoids and univalence
- On the ∞$\infty$‐topos semantics of homotopy type theory
- Homotopy type theory: the logic of space
- Mini-workshop: The homotopy interpretation of constructive type theory. Abstracts from the mini-workshop held February 27th-March 05th, 2011.
- Type theory and homotopy
- The simplicial model of univalent foundations (after Voevodsky)
- Mathesis Universalis and Homotopy Type Theory
- Der Code der Mathematik
- Introduction -- from type theory and homotopy theory to univalent foundations
- Brouwer's fixed-point theorem in real-cohesive homotopy type theory
- Homotopy Type Theory: A synthetic approach to higher equalities
- Homotopy type theory
- Homotopy type theory and the formalization of mathematics
- 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
- Homotopy type theory. Univalent foundations of mathematics
- Higher inductive types as homotopy-initial algebras
- Higher Structures in Homotopy Type Theory
- Idempotents in intensional type theory
- Cubical methods in homotopy type theory and univalent foundations
- A meaning explanation for HoTT
- Univalent foundations of mathematics
- Categorical structures for type theory in univalent foundations
- Towards a constructive simplicial model of Univalent Foundations
- Homotopy type theory in Lean
- Wild \(\omega\)-categories for the homotopy hypothesis in type theory
- 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
- scientific article; zbMATH DE number 7204300 (Why is no real title available?)
- Non-wellfounded trees in homotopy type theory
- Preface to the MSCS Issue 31.1 (2021) Homotopy type theory and univalent foundations. II
- An introduction to univalent foundations for mathematicians
- An experimental library of formalized mathematics based on the univalent foundations
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)
