Homotopy type theory and Voevodsky’s univalent foundations

DOI10.1090/S0273-0979-2014-01456-9zbMath1432.03019arXiv1210.5658OpenAlexW2962780223MaRDI QIDQ2933829

Michael A. Warren, Álvaro Pelayo

Publication date: 8 December 2014

Published in: Bulletin of the American Mathematical Society (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1210.5658

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Categorical logic, topoi (03G30) Abstract and axiomatic homotopy theory in algebraic topology (55U35) Topological categories, foundations of homotopy theory (55U40) Type theory (03B38) Categories of fibrations, relations to (K)-theory, relations to type theory (18N45)

Related Items (8)

Formal Universes ⋮ Observability in the univalent universe ⋮ On the ∞$\infty$‐topos semantics of homotopy type theory ⋮ Idempotents in intensional type theory ⋮ A univalent formalization of the p-adic numbers ⋮ The simplicial model of univalent foundations (after Voevodsky) ⋮ A meaning explanation for HoTT ⋮ Topological model of neural information networks

Uses Software

• Coq

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A model of type theory in simplicial sets. A brief introduction to Voevodsky's homotopy type theory
• Martin-Löf complexes
• Combinatorial realizability models of type theory
• Algebraic classification of equivariant homotopy 2-types. I
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Computer theorem proving in mathematics
• Group-like structures in general categories. I. Multiplications and comultiplications
• A history of algebraic and differential topology 1900--1960
• The identity type weak factorisation system
• The calculus of constructions
• Spaces with finitely many non-trivial homotopy groups
• 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
• Zur Deutung der intuitionistischen Logik
• A set of postulates for the foundation of logic. II
• An \(\omega\)-category with all duals is an \(\omega\)-groupoid
• Homotopical algebra
• Homologie singulière des espaces fibrés. Applications
• Weak omega-categories from intensional type theory
• Types are weak ω -groupoids
• Symplectic theory of completely integrable Hamiltonian systems
• Voevodsky’s Univalence Axiom in Homotopy Type Theory
• On c.s.s. Complexes
• Locally cartesian closed categories and type theory
• Homotopy theoretic models of identity types
• Cosmoi of Internal Categories
• Functionality in Combinatory Logic
• Coherence for tricategories
• Type Theory and Homotopy
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
• Higher Topos Theory (AM-170)
• A univalent formalization of the p-adic numbers
• A formulation of the simple theory of types
• The Calculi of Lambda Conversion. (AM-6)
• Algebraic Operads

This page was built for publication: Homotopy type theory and Voevodsky’s univalent foundations