# Start a new discussion

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorDavid_Corfield
• CommentTimeJan 14th 2021

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