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.