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).
Added topological complexity of tori.
It may be time to create at least a minimum entry on topological complexity, as you keep pointing to it.
I am already on it. The page will be published within the next hour.
1 to 5 of 5