Homotopy type theory. Univalent foundations of mathematics
From MaRDI portal
(Redirected from Publication:5420262)
Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Categorical logic, topoi (03G30) Foundations, relations to logic and deductive systems (18A15) Categories of sets, characterizations (18B05) Research exposition (monographs, survey articles) pertaining to algebraic topology (55-02) Topological categories, foundations of homotopy theory (55U40)
Abstract: Homotopy type theory is a new branch of mathematics, based on a recently discovered connection between homotopy theory and type theory, which brings new ideas into the very foundation of mathematics. On the one hand, Voevodsky's subtle and beautiful "univalence axiom" implies that isomorphic structures can be identified. On the other hand, "higher inductive types" provide direct, logical descriptions of some of the basic spaces and constructions of homotopy theory. Both are impossible to capture directly in classical set-theoretic foundations, but when combined in homotopy type theory, they permit an entirely new kind of "logic of homotopy types". This suggests a new conception of foundations of mathematics, with intrinsic homotopical content, an "invariant" conception of the objects of mathematics -- and convenient machine implementations, which can serve as a practical aid to the working mathematician. This book is intended as a first systematic exposition of the basics of the resulting "Univalent Foundations" program, and a collection of examples of this new style of reasoning -- but without requiring the reader to know or learn any formal logic, or to use any computer proof assistant.
Recommendations
Cited in
(only showing first 100 items - show all)- The future of mathematics in economics: a philosophically grounded proposal
- Aligning concepts across proof assistant libraries
- Game semantics for dependent types
- Decomposition spaces, incidence algebras and Möbius inversion. I: Basic theory
- Univalent completion
- Homotopy type theory in Lean
- Constructive knowledge and the justified true belief paradigm
- To be or not to be constructive, that is not the question
- Klein-Weyl's program and the ontology of gauge and quantum systems
- Carnap and the invariance of logical truth
- Bousfield localisation and colocalisation of one-dimensional model structures
- Fibrational modal type theory
- The homotopy theory of type theories
- Univalence as a principle of logic
- Combinatorial topology and constructive mathematics
- New perspectives on the hole argument
- The hole argument in homotopy type theory
- The hole argument, take \(n\)
- Univalent polymorphism
- Foreword to the special focus on formal proofs for mathematics and computer science
- Construction of the circle in \textit{UniMath}
- The simplicial model of univalent foundations (after Voevodsky)
- A constructive approach to Freyd categories
- Filter quotients and non-presentable \((\infty,1)\)-toposes
- A meaning explanation for HoTT
- The structuralist mathematical style: Bourbaki as a case study
- Predicativity and constructive mathematics
- Rensets and renaming-based recursion for syntax with bindings
- Univalence and completeness of Segal objects
- Reflections on the foundations of mathematics. Univalent foundations, set theory and general thoughts. Based on the conference on foundations of mathematics: univalent foundations and set theory, FOMUS, Bielefeld, Germany, July 18--23, 2016
- Constructive mathematics, Church's thesis, and free choice sequences
- On representations of intended structures in foundational theories
- Left-exact localizations of \(\infty\)-topoi. I: Higher sheaves
- From reversible programs to univalent universes and back
- Finitary higher inductive types in the groupoid model
- A characterisation of elementary fibrations
- The construction of set-truncated higher inductive types
- Homotopical inverse diagrams in categories with attributes
- Graph theory in Coq: minors, treewidth, and isomorphisms
- What inductive explanations could not be
- Composition of deductions within the propositions-as-types paradigm
- Classical misuse attacks on NIST round 2 PQC. The power of rank-based schemes
- Characterizations of modalities and lex modalities
- The Cantor-Schröder-Bernstein theorem for -groupoids
- Constructing a universe for the setoid model
- On abstraction in mathematics and indefiniteness in quantum mechanics
- Combinatorial structure of type dependency
- The justification of identity elimination in Martin-Löf's type theory
- Preface: Special issue on homotopy type theory and univalent foundations
- Canonicity for cubical type theory
- Guarded cubical type theory
- The James construction and \(\pi _4(\mathbb{S}^{3})\) in homotopy type theory
- From signatures to monads in \textsf{UniMath}
- Categoricity results and large model constructions for second-order ZF in dependent type theory
- First steps towards a formalization of forcing
- On endotrivial modules for Lie superalgebras
- Formalizing mathematical knowledge as a biform theory graph: a case study
- Internal languages of finitely complete ( , 1)-categories
- An implementation of effective homotopy of fibrations
- General proof theory: introduction
- Observability in the univalent universe
- Formalizing CCS and \(\pi\)-calculus in Guarded Cubical Agda
- Identity and intensionality in univalent foundations and philosophy
- Type-theoretic approaches to ordinals
- Towards a homotopy domain theory
- Category theory, logic and formal linguistics: some connections, old and new
- Exercising Nuprl's open-endedness
- Canonicity of weak -groupoid laws using parametricity theory
- A constructive manifestation of the Kleene-Kreisel continuous functionals
- The intrinsic topology of Martin-Löf universes
- Homotopy type theory and Voevodsky's univalent foundations
- Homotopy Type Theory
- The local universes model: an overlooked coherence construction for dependent type theories
- Proof assistants for natural language semantics
- Polynomial functors and combinatorial Dyson-Schwinger equations
- Homotopy type theory and the formalization of mathematics
- Automorphisms of types in certain type theories and representation of finite groups
- A homotopy-theoretic model of function extensionality in the effective topos
- A type theory for synthetic -categories
- The Cayley-Dickson construction in homotopy type theory
- Displayed categories
- Natural models of homotopy type theory
- True V or Not True V, That Is the Question
- Effective validity: a generalized logic for stable approximate inference
- Mathesis Universalis and Homotopy Type Theory
- From mathesis universalis to provability, computability, and constructivity
- Does homotopy type theory provide a foundation for mathematics?
- Computational logic: its origins and applications
- Algorithmic theories of problems. A constructive and a non-constructive approach
- Foundations of dependent interoperability
- Heterogeneous substitution systems revisited
- Towards a cubical type theory without an interval
- Cubical type theory: a constructive interpretation of the univalence axiom
- A synopsis of morphoid type theory
- scientific article; zbMATH DE number 7003193 (Why is no real title available?)
- Models of type theory based on Moore paths
- Denotational semantics of recursive types in synthetic guarded domain theory
- Brouwer's fixed-point theorem in real-cohesive homotopy type theory
- Validating Brouwer's continuity principle for numbers using named exceptions
- Categorical structures for type theory in univalent foundations
This page was built for publication: Homotopy type theory. Univalent foundations of mathematics
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5420262)
