In computer science, there is a notion of cyclic lists, which are typically implemented using pointers or modular arithmetic. Mathematically, we may define the set of 2-cycles of elements from a set $A$ as the quotient of $A\times A$ by the relations $(a_0,a_1)\sim(a_1,a_0)$. Similarly we may define the set of 3-cycles as the quotient of $A\times A\times A$ by the relations $(a_0,a_1,a_2)\sim(a_1,a_2,a_0)$. In homotopy type theory, the idea is to view all data types as "topological spaces", and it is possible to define the (pointed) circle $S^1$ as a data type.


In ordinary topology, let $S^1$ be the circle.

Define the quotient $C_2 :=S^1\times S^1/\sim$ where the equivalence relation $\sim$ is generated by $$(a_0,a_1)\sim(a_1,a_0)\qquad(a_0,a_1\in S^1).$$ What surface is it?

Similarly for $C_3 := S^1\times S^1\times S^1/\sim$ where the equivalence relation $\sim$ is generated by $$(a_0,a_1,a_2)\sim(a_1,a_2,a_0)\qquad(a_0,a_1,a_2\in S^1);$$ Can we identify this 3-dimensional space?

  • 3
    $\begingroup$ The first is a Mobius band. I've given that answer here. $\endgroup$ Jul 29 '19 at 22:13
  • 2
    $\begingroup$ For $C_3$, you can regard the $S^1 \times S^1 \times S^1$ as a quotient of the unit cube where you identify opposite faces. That might be fruitful. You might also be interested in the notion of symmetric product $\endgroup$ Jul 29 '19 at 22:15
  • $\begingroup$ In ordinary topology, one can form the quotients of these actual topological spaces by these equivalence relations; this is the context of Andres's linked answer. In homotopy type theory, it's more accurate to say that types are viewed as $\infty$-groupoids, and the notion of "quotient" is much more subtle: instead of "identifying" points it's usually better to think of "gluing in a path" between them (a homotopy colimit), and then you have to think about whether you want to glue in higher coherence paths as well. Which of these questions did you mean to ask? $\endgroup$ Jul 31 '19 at 10:01
  • $\begingroup$ I expected an answer to the former question. But I would also be interested in whether that answer agrees with what you get when you define a higher inductive type with a single point constructor and a single path constructor. $\endgroup$ Jul 31 '19 at 10:40
  • $\begingroup$ I note that the HIT of 3-cycles of elements of unit type (with only two constructors) is S^1, and the ordinary space of 3-cycles of elements from the singleton space is not S^1. It would be interesting to hear what higher coherence paths you would try in general. $\endgroup$ Jul 31 '19 at 11:13

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.