An introduction to univalent foundations for mathematicians
From MaRDI portal
Abstract: We offer an introduction for mathematicians to the univalent foundations of Vladimir Voevodsky, aiming to explain how he chose to encode mathematics in type theory and how the encoding reveals a potentially viable foundation for all of modern mathematics that can serve as an alternative to set theory.
Recommendations
Cites work
- A C-system defined by a universe category
- A formal proof of the Kepler conjecture
- A generalized Blakers–Massey theorem
- A machine-checked proof of the odd order theorem
- A mechanization of the Blakers-Massey connectivity theorem in homotopy type theory
- A system of axiomatic set theory—Part II
- An experimental library of formalized mathematics based on the univalent foundations
- Brouwer's fixed-point theorem in real-cohesive homotopy type theory
- C-systems defined by universe categories: presheaves
- Calculating the Fundamental Group of the Circle in Homotopy Type Theory
- Computational higher-dimensional type theory
- Cubical type theory: a constructive interpretation of the univalence axiom
- Every planar map is four colorable. I: Discharging
- Every planar map is four colorable. II: Reducibility
- Formal proof - the four color theorem
- Goodwillie's calculus of functors and higher topos theory
- Homotopy theoretic models of identity types
- Homotopy type theory. Univalent foundations of mathematics
- scientific article; zbMATH DE number 6694181 (Why is no real title available?)
- scientific article; zbMATH DE number 3859117 (Why is no real title available?)
- scientific article; zbMATH DE number 3521950 (Why is no real title available?)
- scientific article; zbMATH DE number 1136106 (Why is no real title available?)
- scientific article; zbMATH DE number 3331288 (Why is no real title available?)
- scientific article; zbMATH DE number 3365218 (Why is no real title available?)
- I. M. Gelfand and his seminar -- a presence
- On higher inductive types in cubical type theory
- Products of families of types and (Pi,lambda)-structures on C-systems
- Propositions as [Types]
- Structural analysis of narratives with the Coq proof assistant
- Subsystems and regular quotients of C-systems
- The (Pi,lambda)-structures on the C-systems defined by universe categories
- The James construction and \(\pi _4(\mathbb{S}^{3})\) in homotopy type theory
- The law of excluded middle in the simplicial model of type theory
- The Seifert-van Kampen Theorem in Homotopy Type Theory
- Theory of dependent types and axiom of univalence
- Univalent categories and the Rezk completion
- Univalent foundations as structuralist foundations
Cited in
(24)- Univalent foundations as structuralist foundations
- Univalence as a principle of logic
- The simplicial model of univalent foundations (after Voevodsky)
- A meaning explanation for HoTT
- 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
- Homotopy type theory and Voevodsky's univalent foundations
- Homotopy type theory and the formalization of mathematics
- scientific article; zbMATH DE number 3179415 (Why is no real title available?)
- Does homotopy type theory provide a foundation for mathematics?
- scientific article; zbMATH DE number 7474655 (Why is no real title available?)
- Univalent foundations of mathematics and paraconsistency
- An experimental library of formalized mathematics based on the univalent foundations
- The Unification of Mathematics via Topos Theory
- Naïve Type Theory
- Univalent Foundations and the UniMath Library
- A New Foundational Crisis in Mathematics, Is It Really Happening?
- Prolegomena to virtue-theoretic studies in the philosophy of mathematics
- Der Code der Mathematik
- Internal sums for synthetic fibered (,1)-categories
- Two-sided Cartesian fibrations of synthetic \((\infty, 1)\)-categories
- Kolmogorov's Calculus of Problems and its Legacy
- Accepted proofs: objective truth, or culturally robust?
- The univalence principle
- Scott's representation theorem and the univalent Karoubi envelope
Describes a project that uses
Uses Software
This page was built for publication: An introduction to univalent foundations for mathematicians
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4684362)
