¿Cómo puedo construir $\mathbb{S}^1$ en Homotopy Tipo de Teoría a través de pushouts?

Question

Supongamos que yo tome la $0$-esqueleto $X_0$ tener un solo habitante $base$.

Deje $S_1$ tienen un solo punto de $base'$, con la fijación de mapa $f(base', -)=base$. Si construyo el pushout para el 1-esqueleto $X_1$, como abajo, $$ \requieren{AMScd} \begin{CD} S_1 \times \mathbb{S}^0 @>{f}>> X_0;\\ @VVV @VVV \\ \mathbf{1} @>>> X_1; \end{CD} $$ Termino con $X_1$ definido por

• $inl: \mathbf{1} \rightarrow X_1$
• $inr: X_0 \rightarrow X_1 $
• para cada una de las $c:S_1 \times \mathbb{S}^0$, un camino de $inl(\star) = inr(base)$

Este es el tipo de intervalo, aunque! Donde he ido mal en mi construcción?

Answer 1

Nada de malo en su construcción. No obtener el intervalo ya que no hay manera de probar que los dos caminos son iguales. Para mayor claridad, tenga en cuenta que $\mathbb{S}^1$ como un pushout es simplemente el pushout de la siguiente span

$$ \begin{CD} \mathbb{S^0} @>>> \mathbf{1} \\ @VVV \\ \mathbf{1} \end{CD} $$, donde $\mathbf{1}$ es el tipo de unidad y $\mathbb{S}^0$ es el tipo de booleanos (o el subproducto $\mathbf{1}\coprod\mathbf{1}$ si quieres).

Answer 2

No veo por qué decimos que este es el tipo de intervalo. Hay dos puntos en $S_0\times \mathbb{S}^0$, para llegar a las rutas de acceso entre los dos puntos dados, que es de hecho una forma de describir el círculo.