The Equivalence of the Torus and the Product of Two Circles in Homotopy Type Theory
Abstract
Homotopy type theory is a new branch of mathematics that merges insights from abstract homotopy theory and higher category theory with those of logic and type theory. It allows us to represent a variety of mathematical objects as basic type-theoretic construction, higher inductive types. We present a proof that in homotopy type theory, the torus is equivalent to the product of two circles. This result indicates that the synthetic definition of torus as a higher inductive type is indeed correct.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Nov 03, 2016
- Source ID
- 10.1145/2992783
Entities
People
- Kristina Sojakova
Organizations
- Air Force Office of Scientific Research
- Carnegie Mellon University