How to code a Mobius strip with this?

[garyzhubc]

How to code a Mobius strip with this?

[iblech]

Are you familiar with the universal cover of $S^1$, the helix? This can be obtained as the total space of the type family $S^1 \to \mathrm{Type}$ which maps the base point to $\mathbb{Z}$ and $\mathsf{loop}$ to the equality obtained via univalence from the equivalence $\mathsf{succ} : \mathbb{Z} \to \mathbb{Z}$.

The Möbius strip can be constructed in a similar fashion: Use the unit interval in place of $\mathbb{Z}$ and its reversal equivalence. But note that the Möbius strip is homotopy equivalent to the circle. Hence you will not obtain a "new" type with this construction, just a different presentation of an already existing one.

Instead of the unit interval, you could also use the type $\mathrm{Bool}$ with its equivalence $\mathsf{not} : \mathrm{Bool} \to \mathrm{Bool}$. In this fashion you obtain the boundary of the Möbius strip, i.e. the double cover of $S^1$.

Feel free to ask for clarification in case you are not familiar with some of the terms in this answer :-)