This summer I did research at Inria Nantes with the people in the CoqHoTT group, in particular with Nicolas Tabareau and Simon Boulier. Specifically, we worked on a coinductive approach to -equivalence relations, about which I’ll give a talk tomorrow at the CMU HoTT seminar. Thus, I had to learn how to handle coinductive types, and in this blog post I want to tell some folklore results about one particular aspect of coinductive types: their identity types!
The most basic example of a coinductive type is the type of streams in a given type . A stream in can be thought of as an infinite string of terms of , indexed by the natural numbers. There are two basic operations one can perform on streams, that characterize what streams are: one can take the head of a stream, which is the term at position 0, or one can take the tail of a stream, which is the stream one gets by removing the term at position 0. Thus, we have a map . In fact, this map is an equivalence.
Now note that we have an endofunctor given by , which can be thought of as a linear polynomial. A coalgebra for is an object together with a map , which is in our case a type together with a map . Thus, we see that the type of streams is a coalgebra for the endofunctor . Indeed, it is defined as the final coalgebra (i.e. a terminal object in the category of coalgebras for ).
To model general coinductive types, we have to talk about containers. A (small) container is just a type together with a type family . Each container determines a polynomial endofunctor by . The coinductive type associated to the container is then defined to be the final coalgebra for . One expresses the condition of being final in HoTT, simply by saying that for each coalgebra of , the type of coalgebra homomorphisms from to is contractible. Under this condition, one can show that the map is an equivalence.
Coinductive types as limits
The immediate question is then whether such final coalgebras always exist in the setting of homotopy type theory, and this is indeed the case. Ahrens, Capriotti and Spadotti have formalized a construction of final coalgebras, as the limit of a simple diagram obtained by iteratively applying to the unit type :
We denote the maps in this diagram by .
For future reference, it will be useful to have an explicit description of the coalgebra structure of . That is, we want to give a precise definition of the map . Note that decomposes into a map and a dependent function . Let , where , and where .
- First, we define .
- The construction of is a bit more involved. We will construct the map by constructing a cone on the defining diagram of . This cone is obtained by constructing a natural transformation of type sequences
in which the vertical maps are given by , and the horizontal maps on the top row are required to be equivalences. We obtain the commuting squares by generalization. Note that for each , we have and such that . More generally, suppose we have and such that . We want to show that the diagram
commutes, where the top map is an equivalence. Since the endpoint of the path is free, we may eliminate it into . Also, note that . Thus, we want to make a commuting diagram of the form
which is straightforward, since we may take the upper map to be the identity map.
This finishes the construction of . Before we continue, let us review a bit of the theory of limits in HoTT.
Limits in HoTT
Recall from the previous post, that a graph consists of a type of vertices and a binary, type-valued relation of edges. A diagram over the graph then consists of a type family , and an indexed family of maps . Any type determines a diagram on . A cone on with vertex is then simply a morphism of diagram . By functoriality of , we get for each a map , and pre-composing by gives an operation from cones with vertex to cones with vertex . A cone with vertex is said to be limiting if for each , this precomposition map is an equivalence. A limiting cone always exists, since we can take the type to be the type of pairs , where
Of course, the proof that this cone is limiting uses the principle of function extensionality, but that is basically all there is to it. Now we can also easily compute the identity type of the limit:
Lemma 1. For any , the identity type is equivalent to the limit of the diagram over , defined by
Identity types of coinductive types
Theorem 2. Let be an indexed container, and let . Then the following are equivalent types:
- The type .
- The type of pairs consisting of and . Here and are the first and second component of the map .
- The limit of the type sequence
where the maps are given by .
The last description of the identity type looks suspiciously much like the sequence that Ahrens, Capriotti and Spadotti used to define the coinductive types. That is precisely what we’re after: a description of the identity type of a coinductive type as a certain other coinductive type, the bisimilation relation! However, the bisimilation relation is not just an ordinary coinductive type of the kind we described above. It is rather an indexed coinductive type, so we need indexed containers. It is a bit of extra machinery, but it will be worth it!
An indexed container consists of a type , a type family , a further type family , and a re-indexing function . Just like ordinary containers, an indexed container determines a polynomial endofunctor acting on the category . It is defined by
Again, the functorial action of is given by precomposition. As with ordinary containters, one can construct the final coalgebra for as the limit of the type sequence
Here, indicates the constant type family over with value .
Our goal is to define an indexed container that defines the bisimilation relation as a coinductive type. Note that we can basically read off from the second equivalent description of the identity type of in Theorem 2 what and should be:
- For the indexing type we take .
- We define .
- We define .
- We define the re-indexing function by .
Now let us compute the action of the polynomial functor explicitly. We have
Note that the third description in Theorem 2 already states that the type family is a coalgebra for latex . Now it is pretty straightforward to show that it is also final. What needs to be done is to construct a natural equivalence of the defining type sequence of , and the type sequence of Theorem 2. In other words, one has to show that we have a diagram of the form
Update 10/17/2016: Included an explicit description of the coalgebra structure of .