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$, from`base`

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).