The equivalence of the torus and the product of two circles in homotopy type theory

TL;DR

This paper proves within homotopy type theory that the torus is equivalent to the product of two circles, confirming the correctness of the synthetic definition of the torus as a higher inductive type.

Contribution

It provides a formal proof of the equivalence between the torus and the product of two circles in homotopy type theory, validating the synthetic approach.

Findings

The torus is equivalent to the product of two circles in homotopy type theory.

The synthetic definition of the torus as a higher inductive type is correct.

The proof bridges abstract homotopy theory and type-theoretic representations.

Abstract

Homotopy type theory is a new branch of mathematics which 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 constructions, 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.