How can I construct $\mathbb{S}^1$ in Homotopy Type Theory via pushouts?

Question

Suppose I take the $0$-skeleton $X_0$ to have a single inhabitant $base$.

Let $S_1$ have a single point $base'$, with attaching map $f(base', -)=base$. If I construct the pushout to the 1-skeleton $X_1$, as below, $$ \require{AMScd} \begin{CD} S_1 \times \mathbb{S}^0 @>{f}>> X_0;\\ @VVV @VVV \\ \mathbf{1} @>>> X_1; \end{CD} $$ I end up with $X_1$ defined by

• $inl: \mathbf{1} \rightarrow X_1$
• $inr: X_0 \rightarrow X_1 $
• for each $c:S_1 \times \mathbb{S}^0$, a path $inl(\star) = inr(base)$

This is the interval type though! Where have I gone wrong in my construction?

Answer 1

I don't see why you say this is the interval type. There are two points in $S_0\times \mathbb{S}^0$, so you get to paths between the two given points, which is indeed a way of describing the circle.

Answer 2

Nothing wrong in your construction. You don't get the interval since there is no way even to prove that your two paths are equal. For clarity, note that $\mathbb{S}^1$ as a pushout is simply the pushout of the following span

$$ \begin{CD} \mathbb{S^0} @>>> \mathbf{1} \\ @VVV \\ \mathbf{1} \end{CD} $$, where $\mathbf{1}$ is the unit type and $\mathbb{S}^0$ is the type of booleans (or the coproduct $\mathbf{1}\coprod\mathbf{1}$ if you wish).