Cómo mostrar la doble cubierta de $S^1$ es un círculo en HoTT

Question

Considere la familia $E : S^1 \to \mathcal{U}$ para que

• $E(\mathtt{base}) = \mathbf{2}$
• $\text{apd}_E(\mathtt{loop}) = \mathtt{ua}(\lnot)$

donde, por supuesto, $\lnot : \mathbf{2} \simeq \mathbf{2}$ intercambia los dos elementos.

Es geométricamente claro que esto debería ser el análogo teórico de tipo del clásico $z \mapsto z^2$ doble cubierta, pero me cuesta demostrar que el espacio total es realmente un círculo. Es decir:

$$\sum_{x : S^1} E(x) \simeq S^1$$

Creo que puedo hacerlo si sabemos que el HIT dado por dos puntos y dos caminos:

• $\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}$

es equivalente a $S^1$ que, de nuevo, es geométricamente claro. Pero también me cuesta demostrarlo.

Se agradece cualquier ayuda ^_^

Answer 1

Permítanme esbozar cómo se podría construir la equivalencia directamente.

Dar un mapa $f : (\sum_{x : S^1} E (x)) \to T$ es lo mismo que dar un elemento $f (x, e) : T$ para cada $x : S^1$ y $e : E (x)$ . Por inducción, es lo mismo que dar $f (\textrm{base}, \textrm{base}_1) : T$ , $f (\textrm{base}, \textrm{base}_2) : T$ un camino $f (\textrm{base}, \textrm{base}_1) =_T f (\textrm{base}, \textrm{base}_2)$ y una ruta $f (\textrm{base}, \textrm{base}_2) =_T f (\textrm{base}, \textrm{base}_1)$ . (Quizá esto dependa de lo estricto que sea su axioma de univalencia). En el caso de que $T$ es $S^1$ no hay muchas opciones; una que funciona es tomar $f (\textrm{base}, \textrm{base}_1)$ y $f (\textrm{base}, \textrm{base}_2)$ tanto para ser $\textrm{base}$ un camino para ser $\textrm{refl}_\textrm{base}$ y el otro $\textrm{loop}$ .

Dar un mapa $g : S^1 \to \sum_{x : S^1} E (x)$ es mucho más fácil: basta con enviar $\textrm{base}$ a $(\textrm{base}, \textrm{base}_1)$ y $\textrm{loop}$ a la trayectoria trazada por el transporte $(\textrm{base}, \textrm{base}_1)$ en $\textrm{loop}$ dos veces.

Debería ser sencillo comprobar que $f$ y $g$ son mutuamente inversos, pero admito que no lo he intentado (así que quizá haya que ocuparse de algunas cosas tediosas porque no tenemos tantas igualdades estrictas como nos gustaría).