The simplest kind of coinductive types are described by containers. Recall that a container is just a type $latex A$ with a type family $latex 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 … Continue reading The coinductive type generated by the universal bundle of a pointed connected type