How to show the double cover of $S^1$ is a circle in HoTT Consider the family $E : S^1 \to \mathcal{U}$ so that

*

*$E(\mathtt{base}) = \mathbf{2}$

*$\text{apd}_E(\mathtt{loop}) = \mathtt{ua}(\lnot)$
where, of course, $\lnot : \mathbf{2} \simeq \mathbf{2}$ swaps the two elements.
It's geometrically clear that this should be type theoretic analogue of the classical $z \mapsto z^2$ double cover, but I'm struggling to prove that the total space really is a circle. That is:
$$\sum_{x : S^1} E(x) \simeq S^1$$
I think I can do it if we know that the HIT given by two points and two paths:

*

*$\mathtt{base_1} : (S^1)'$

*$\mathtt{base_2} : (S^1)'$

*$\mathtt{p_1} : \mathtt{base_1} = \mathtt{base_2}$

*$\mathtt{p_2} : \mathtt{base_2} = \mathtt{base_1}$
is equivalent to $S^1$, which again, is geometrically clear. But I'm struggling to prove it too.
Any help is appreciated ^_^
 A: Let me sketch how one might construct the equivalence directly.
Giving a map $f : (\sum_{x : S^1} E (x)) \to T$ is the same as giving an element $f (x, e) : T$ for every $x : S^1$ and $e : E (x)$.
By induction, it is the same as giving $f (\textrm{base}, \textrm{base}_1) : T$, $f (\textrm{base}, \textrm{base}_2) : T$, a path $f (\textrm{base}, \textrm{base}_1) =_T f (\textrm{base}, \textrm{base}_2)$, and a path $f (\textrm{base}, \textrm{base}_2) =_T f (\textrm{base}, \textrm{base}_1)$.
(Maybe this depends on how strict your univalence axiom is.)
In the case where $T$ is $S^1$ there are not many choices; one choice that works is to take $f (\textrm{base}, \textrm{base}_1)$ and $f (\textrm{base}, \textrm{base}_2)$ both to be $\textrm{base}$, one path to be $\textrm{refl}_\textrm{base}$, and the other to be $\textrm{loop}$.
Giving a map $g : S^1 \to \sum_{x : S^1} E (x)$ is much easier: just send $\textrm{base}$ to $(\textrm{base}, \textrm{base}_1)$ and $\textrm{loop}$ to the path traced by transporting $(\textrm{base}, \textrm{base}_1)$ over $\textrm{loop}$ twice.
It should be straightforward to verify that $f$ and $g$ are mutually inverse, but I admit I haven't tried (so maybe there are some tedious things to take care of because we don't have as many strict equalities as we would like).
