natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
homotopy theory, (∞,1)-category theory, homotopy type theory
flavors: stable, equivariant, rational, p-adic, proper, geometric, cohesive, directed…
models: topological, simplicial, localic, …
see also algebraic topology
Introductions
Definitions
Paths and cylinders
Homotopy groups
Basic facts
Theorems
This entry collects links related to the forthcoming book
Introduction to Homotopy Type Theory
Cambridge Studies in Advanced Mathematics,
Cambridge University Press
arXiv:2212.11082 (359 pages)
which introduces homotopy type theory in general and in particular Martin-Löf's dependent type theory, the Univalent Foundations for Mathematics and synthetic homotopy theory.
The book is based on a course taught by the author at Carnegie Mellon University in the spring semester of 2018:
The original writeup of these course notes
contains considerably more material than retained in the above arXiv version.
Other versions:
pdf (2019 summer school notes) (134 pages)
pdf (2022 HoTTEST summer school) (478 pages)
Chapter I introduces the reader to Martin-Löf's dependent type theory. The fundamental concepts of type theory are explained without immediately jumping into the homotopy interpretation of type theory.
$\;\;\;1.$ Dependent Type Theory
$\;\;\;2.$ Dependent function types
$\;\;\;3.$ The natural numbers
$\;\;\;4.$ More inductive types
$\;\;\;5.$ Identity types
$\;\;\;6.$ Universes
$\;\;\;7.$ Modular arithmetic via the Curry-Howard isomorphism
$\;\;\;8.$ Decidability in elementary number theory
Chapter II is an exposition of the Univalent Foundations for Mathematics. This chapter gradually extends dependent type theory with function extensionality, propositional truncation, the univalence axiom, and the type theoretic replacement axiom.
$\;\;\;9.$ Equivalences
$\;\;\;10.$ Contractible types
$\;\;\;11.$ The fundamental theorem of identity types
$\;\;\;12.$ Propositions, sets, and the higher truncation levels
$\;\;\;13.$ Function extensionality
$\;\;\;14.$ Propositional truncations
$\;\;\;15.$ Image factorizations
$\;\;\;16.$ Finite types
$\;\;\;17.$ The univalence axiom
$\;\;\;18.$ Set quotients
$\;\;\;19.$ Groups in univalent mathematics
$\;\;\;20.$ General inductive types
Chapter III studies the circle as a higher inductive type.
$\;\;\;21.$ The circle
$\;\;\;22.$ The universal cover of the circle
An older version of the book ended:
$\;\;\;22.$ Homotopy pullbacks
$\;\;\;23.$ Homotopy pushouts
$\;\;\;25.$ Universality and descent for pushouts
$\;\;\;26.$ Sequential colimits
$\;\;\;27.$ Homotopy groups of types
$\;\;\;28.$ The classifying type of a group
$\;\;\;29.$ The Hopf fibration
$\;\;\;30.$ The real projective spaces
$\;\;\;31.$ Truncations
$\;\;\;32.$ Connected types and maps
$\;\;\;33.$ The Blakers-Massey theorem
$\;\;\;34.$ Higher group theory
The main formalization of the book is in Agda.
Parts of the book have also been formalized in Coq.
Last revised on January 3, 2023 at 22:58:15. See the history of this page for a list of all contributions to it.