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

20161018_1

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.

 

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s