Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Added a subsection
As a homotopy type
As a homotopy type the torus is the product of two copies of the circle.
In homotopy type theory the torus can be formalized as the higher inductive type generated by a point
base
, two paths, $p$ and $q$, frombase
to itself, and an element $t$ of $p\cdot q = q \cdot p$. It has been formally shown (Sojakova15) that this type is equivalent to the product of two circles. For a treatment in cubical type theory, see (Licata-Brunierie).
1 to 2 of 2