REVIEW 4 cited by
Introduction to Homotopy Type Theory
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
read the original abstract
This is an introductory textbook to univalent mathematics and homotopy type theory, a mathematical foundation that takes advantage of the structural nature of mathematical definitions and constructions. It is common in mathematical practice to consider equivalent objects to be the same, for example, to identify isomorphic groups. In set theory it is not possible to make this common practice formal. For example, there are as many distinct trivial groups in set theory as there are distinct singleton sets. Type theory, on the other hand, takes a more structural approach to the foundations of mathematics that accommodates the univalence axiom. This, however, requires us to rethink what it means for two objects to be equal. This textbook introduces the reader to Martin-L\"of's dependent type theory, to the central concepts of univalent mathematics, and shows the reader how to do mathematics from a univalent point of view. Over 200 exercises are included to train the reader in type theoretic reasoning. The book is entirely self-contained, and in particular no prior familiarity with type theory or homotopy theory is assumed.
Forward citations
Cited by 4 Pith papers
-
Elementary $\infty$-toposes from type theory
Categorical models of univalent type theory localise to elementary ∞-toposes, and such ∞-toposes automatically have small subobject classifiers.
-
Orthocomplemented subspaces and partial projections on a Hilbert space
Orthocomplemented subspaces of a Hilbert space are in bijection with partial projections, yielding a constructive quantum logic with classical negation.
-
Formalization of the zigzag construction of path spaces of pushouts in homotopy type theory
The zigzag construction for path spaces of arbitrary pushouts is fully formalized in Agda, with a machine-checked proof that it is fiberwise equivalent to the actual path spaces.
-
Synthetic perspectives on spaces and categories
A well-referenced exposition of path and arrow induction plus (directed) univalent universes for synthetic spaces and categories, with small strengthened lemmas and a preview of directed univalence.
Discussion (0). Continue with ORCID to comment.