The simplest kind of coinductive types are described by containers. Recall that a container is just a type with a type family
. 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 be a pointed connected type, with base point
, and let
be the family of paths starting at
, i.e.
. The polynomial endofunctor
is then given by
.
Now we observe that is a pointed type, with base point
, where
is the constant function. In other words, the unit type
is a coalgebra for
! This implies that there is a unique homomorphism of coalgebras from
to
,
and in particular that is again a pointed type. Let
be the base point of
. Then it also follows that
, where
is the constant function pointing to
.
More generally, whenever is pointed type, so is
. From the same argument, it follows that if
is merely inhabited, then so is
(and likewise for indexed coinductive types). Moreover, we get a fiber sequence
.
Now lets think about the identity type of . By the bisimilation theorem, it follows that for any
, the identity type
is equivalent to the coinductive type
, which is the final coalgebra for the polynomial endofunctor associated to the indexed container
,
,
,
.
From this description we see immediately that each is going to be a merely inhabited type, because each
is merely inhabited. In other words, by the assumption that
is (pointed and) connected, it follows that
is (pointed and) connected.
Also, since and
is the constant map pointing to
, we see that
is the final coalgebra for the polynomial endofunctor
.
In other words, is the classifying type of
, where
is the constant family pointing to
.
This gives some fun results in the case of the infinite real and complex projective spaces, where the loop space of is the final coalgebra for
, and
respectively. If people would be up for it, I’d love to try to get a better feeling for what those spaces are.