An introduction to univalent foundations for mathematicians
From MaRDI portal
Publication:4684362
DOI10.1090/bull/1616zbMath1461.03012arXiv1711.01477OpenAlexW2767684089WikidataQ130161971 ScholiaQ130161971MaRDI QIDQ4684362
Publication date: 28 September 2018
Published in: Bulletin of the American Mathematical Society (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1711.01477
Categorical logic, topoi (03G30) Mechanization of proofs and logical operations (03B35) Abstract and axiomatic homotopy theory in algebraic topology (55U35) Foundations, relations to logic and deductive systems (18A15) Type theory (03B38)
Related Items (5)
A New Foundational Crisis in Mathematics, Is It Really Happening? ⋮ Prolegomena to virtue-theoretic studies in the philosophy of mathematics ⋮ Unnamed Item ⋮ The simplicial model of univalent foundations (after Voevodsky) ⋮ A meaning explanation for HoTT
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Every planar map is four colorable. I: Discharging
- Every planar map is four colorable. II: Reducibility
- Univalent foundations as structuralist foundations
- The James construction and \(\pi _4(\mathbb{S}^{3})\) in homotopy type theory
- I. M. Gelfand and His Seminar-A Presence
- Products of families of types and (Pi,lambda)-structures on C-systems
- C-systems defined by universe categories: presheaves
- The (Pi,lambda)-structures on the C-systems defined by universe categories
- Subsystems and regular quotients of C-systems
- Structural Analysis of Narratives with the Coq Proof Assistant
- A C-system defined by a universe category
- Homotopy theoretic models of identity types
- Cubical Type Theory: a constructive interpretation of the univalence axiom
- Goodwillie's calculus of functors and higher topos theory
- A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory
- Brouwer's fixed-point theorem in real-cohesive homotopy type theory
- Propositions as [Types]
- The law of excluded middle in the simplicial model of type theory
- A generalized Blakers–Massey theorem
- On Higher Inductive Types in Cubical Type Theory
- Calculating the Fundamental Group of the Circle in Homotopy Type Theory
- The Seifert-van Kampen Theorem in Homotopy Type Theory
- A FORMAL PROOF OF THE KEPLER CONJECTURE
- A Machine-Checked Proof of the Odd Order Theorem
- Computational higher-dimensional type theory
- Homotopy Type Theory: Univalent Foundations of Mathematics
- Univalent categories and the Rezk completion
- An experimental library of formalized Mathematics based on the univalent foundations
- A system of axiomatic set theory—Part II
This page was built for publication: An introduction to univalent foundations for mathematicians
