Homotopy type theory and Voevodsky's univalent foundations

DOI10.1090/S0273-0979-2014-01456-9zbMATH Open1432.03019arXiv1210.5658OpenAlexW2962780223MaRDI QIDQ2933829FDOQ2933829

Authors: Álvaro Pelayo, Michael A. Warren 

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

• Homotopy type theory
• Homotopy Type Theory
• The simplicial model of univalent foundations (after Voevodsky)
• Univalent foundations of mathematics
• An introduction to univalent foundations for mathematicians

Mathematics Subject Classification ID

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 \(\omega \)-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
• Formal proof
• 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
• The strict \(\omega\)-groupoid interpretation of type theory
• Voevodsky’s Univalence Axiom in Homotopy Type Theory
• A univalent formalization of the \(p\)-adic numbers

Cited In (42)

• Preface: Special issue on homotopy type theory and univalent foundations
• The homotopy theory of type theories
• Homotopy limits in type theory
• The Seifert-van Kampen Theorem in Homotopy Type Theory
• \(\pi _{n }(S ^{n })\) in homotopy type theory
• A univalent formalization of the \(p\)-adic numbers
• Title not available (Why is that?)
• Formal universes
• 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
• Homotopy type theory: the logic of space
• Type theory and homotopy
• Mini-workshop: The homotopy interpretation of constructive type theory. Abstracts from the mini-workshop held February 27th-March 05th, 2011.
• Der Code der Mathematik
• The simplicial model of univalent foundations (after Voevodsky)
• Mathesis Universalis and Homotopy Type Theory
• 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
• Homotopy type theory. Univalent foundations 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
• Higher Structures in Homotopy Type Theory
• 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
• Towards a constructive simplicial model of Univalent Foundations
• Univalent foundations of mathematics
• Categorical structures for type theory in 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
• Title not available (Why is that?)
• 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
• Lawvere-Tierney sheafification in Homotopy Type Theory
• Observability in the univalent universe

Uses Software

• Coq

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)