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

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?

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).

• Thanks! My mistake was that I thought $\mathbb{S}^0$ was a singleton, rather than having two inhabitants. – Dr. John A Zoidberg Jun 28 '17 at 16:47
• How would I construct the interval from a pushout then? – Dr. John A Zoidberg Jun 28 '17 at 16:50
• @Dr.JohnAZoidberg The interval is equivalent to $1$, so it's not clear that that's a meaningful question. For instance, it's a pushout of $1\leftarrow 1\to 1$... – Kevin Carlson Jun 29 '17 at 1:41
• @Dr.JohnAZoidberg, you are welcome! – Anthony Bordg Jun 29 '17 at 12:05

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.

• Is it possible to prove the equivalence of a circle defined by two points and two paths , and the circle defined by $base$ and $loop$? – Dr. John A Zoidberg Jun 28 '17 at 18:10
• @Dr.JohnAZoidberg, yes it is possible and I will be happy to give further details if you open a new question since it is not convenient to answer questions in the comments section. – Anthony Bordg Jun 29 '17 at 12:02