The coinductive type generated by the universal bundle of a pointed connected type

The simplest kind of coinductive types are described by containers. Recall that a container is just a type $A$ with a type family $B : A \to{}U$ . In this blog post, we will go in detail through an example of such a coinductive type, which we naturally get in the setting of homotopy type theory.

Let $A$ be a pointed connected type, with base point $a_0$ , and let $B:A\to{}U$ be the family of paths starting at $a_0$ , i.e. $B(a):= (a_0=a)$ . The polynomial endofunctor $P_{A,B}$ is then given by

$P_{A,B}(X) := \Sigma_{(a:A)}~X^{(a_0=a)}$ .

Now we observe that $P_{A,B}(\mathbf{1})$ is a pointed type, with base point $(a_0, \mathsf{const}(\star))$ , where $\mathsf{const}(\star):B(a_0)\to\mathbf{1}$ is the constant function. In other words, the unit type $\mathbf{1}$ is a coalgebra for $P_{A,B}$ ! This implies that there is a unique homomorphism of coalgebras from $\mathbf{1}$ to $M(A,B)$ ,

and in particular that $M(A,B)$ is again a pointed type. Let $m_0:M(A,B)$ be the base point of $M(A,B)$ . Then it also follows that $\mathsf{destr}(m_0)=(a_0,\mathsf{const}(m_0))$ , where $\mathsf{const}(m_0):B(a_0)\to{}M(A,B)$ is the constant function pointing to $m_0$ .

More generally, whenever $A$ is pointed type, so is $M(A,B)$ . From the same argument, it follows that if $A$ is merely inhabited, then so is $M(A,B)$ (and likewise for indexed coinductive types). Moreover, we get a fiber sequence

$M(A,B)^{\Omega(A)} \hookrightarrow M(A,B) \twoheadrightarrow A$ .

Now lets think about the identity type of $M(A,B)$ . By the bisimilation theorem, it follows that for any $i,j:M(A,B)$ , the identity type $i=j$ is equivalent to the coinductive type $\mathsf{Bisim}_{A,B}(i,j)$ , which is the final coalgebra for the polynomial endofunctor associated to the indexed container

$I:=M(A,B)\times{}M(A,B)$ ,
$A'((x,h),(y,k)):= (\pi_1(x_1)=\pi_1(y_1))$ ,
$B'((x,h),(y,k),p):= (a_0=\pi_1(x_1))$ ,
$k((x,h),(y,k),p,q):=(\mathsf{destr}_1((x,h),q),\mathsf{destr}_1((y,k),q\cdot p))$ .

From this description we see immediately that each $\mathsf{Bisim}_{A,B}(i,j)$ is going to be a merely inhabited type, because each $A'(i,j)$ is merely inhabited. In other words, by the assumption that $A$ is (pointed and) connected, it follows that $M(A,B)$ is (pointed and) connected.

Also, since $\mathsf{destr}_0(m_0)=a_0$ and $\mathsf{destr}_1(m_0)$ is the constant map pointing to $m_0$ , we see that $\mathsf{Bisim}_{A,B}(m_0,m_0)$ is the final coalgebra for the polynomial endofunctor

$X\mapsto{}\Omega(A)\times X^{\Omega(A)}$ .

In other words, $M(A,B)$ is the classifying type of $M(\Omega(A),\mathsf{const}(\Omega(A)))$ , where $\mathsf{const}(\Omega(A))$ is the constant family pointing to $\Omega(A)$ .

This gives some fun results in the case of the infinite real and complex projective spaces, where the loop space of $M(A,B)$ is the final coalgebra for $X\mapsto{} \mathbf{2}\times{} X^{\mathbf{2}}$ , and $X\mapsto{}S^1\times{}X^{S^1}$ respectively. If people would be up for it, I’d love to try to get a better feeling for what those spaces are.

Egbert RIJKE

PhD student at Carnegie Mellon University

The coinductive type generated by the universal bundle of a pointed connected type

Leave a Reply Cancel reply

Share this:

Like this:

Leave a Reply Cancel reply