What I learned this summer about coinductive types

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 \infty-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. A stream in A can be thought of as an infinite string of terms of A, 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 \mathsf{stream}(A)\to{}A\times{}\mathsf{stream}(A).  In fact, this map is an equivalence.

Now note that we have an endofunctor P given by X\mapsto{} A\times X, which can be thought of as a linear polynomial.  A coalgebra for P is an object X together with a map X\to{} P(X), which is in our case a type X together with a map X\to{} A\times X. Thus, we see that the type of streams is a coalgebra for the endofunctor X\mapsto{} A\times X. Indeed, it is defined as the final coalgebra (i.e. a terminal object in the category of coalgebras for P).

To model general coinductive types, we have to talk about containers. A (small) container is just a type A together with a type family B : A\to{} U. Each container determines a polynomial endofunctor P_{A,B} by X \mapsto{} \Sigma_{(a:A)}X^{B(a)}. The coinductive type \mathsf{M}(A,B) associated to the container (A,B) is then defined to be the final coalgebra (\mathsf{M}(A,B),\mathsf{destr}_{A,B}) for P_{A,B}. One expresses the condition of being final in HoTT, simply by saying that for each coalgebra (X,d) of P_{A,B}, the type of coalgebra homomorphisms from (X,d) to (\mathsf{M}(A,B),\mathsf{destr}_{A,B}) is contractible. Under this condition, one can show that the map \mathsf{destr}_{A,B} 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 P_{A,B} to the unit type \mathbf{1}:

\cdots{} \longrightarrow{} P_{A,B}^2(\mathbf{1}) \longrightarrow{} P_{A,B}(\mathbf{1}) \longrightarrow{} \mathbf{1}

We denote the maps in this diagram by u_n:P_{A,B}^{n+1}(\mathbf{1})\to P_{A,B}^n(\mathbf{1}).

For future reference, it will be useful to have an explicit description of the coalgebra structure of M(A,B). That is, we want to give a precise definition of the map \mathsf{destr}:M(A,B)\to{} P_{A,B}(M(A,B)). Note that \mathsf{destr} decomposes into a map \mathsf{destr}_0 : M(A,B)\to A and a dependent function \mathsf{destr}_1:\Pi_{((x,h):M(A,B))}~(B(\mathsf{destr}_0(x,h)\to{}M(A,B)). Let (x,h):M(A,B), where x : \Pi_{(n:\mathbb{N})}~P^n_{A,B}(\mathbf{1}), and where h:\Pi_{(n:\mathbb{N})}~u_{n}(x_{n+1})=x_n.

  • First, we define \mathsf{destr}_0(x,h):=\pi_1(x_1).
  • The construction of \mathsf{destr}_1(x,h):B(\mathsf{proj}_1(x_1))\to M(A,B) is a bit more involved. We will construct the map \mathsf{destr}_1(x,h):B(\mathsf{proj}_1(x_1))\to M(A,B) by constructing a cone on the defining diagram of M(A,B). This cone is obtained by constructing a natural transformation of type sequences

    20161006_2
    in which the vertical maps are given by \pi_2(x_{n+1}), and the horizontal maps on the top row are required to be equivalences. We obtain the commuting squares by generalization. Note that for each n:\mathbb{N}, we have x_{n+2}:P^{n+2}_{A,B}(\mathbf{1}) and x_{n+1}:P^{n+1}_{A,B}(\mathbf{1}) such that u_{n+1}(x_{n+2})=x_{n+1}. More generally, suppose we have (a,f):P^{n+2}_{A,B}(\mathbf{1}) and (b,g):P^{n+1}_{A,B} such that u_{n+1}(a,f)=(b,g). We want to show that the diagram

    20161006_3.png
    commutes, where the top map is an equivalence. Since the endpoint of the path u_{n+1}(a,f)=(b,g) is free, we may eliminate it into \mathsf{refl}(u_{n+1}(a,f)). Also, note that u_{n+1}(a,f):=(a,u_n\circ f). Thus, we want to make a commuting diagram of the form

    20161006_4
    which is straightforward, since we may take the upper map to be the identity map.

This finishes the construction of \mathsf{destr}:M(A,B)\to{}P_{A,B}(M(A,B)). 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 \Gamma consists of a type \Gamma_0 of vertices and a binary, type-valued relation \Gamma_1:\Gamma_0\to\Gamma_0\to{}U of edges. A diagram D over the graph \Gamma then consists of a type family D_0: \Gamma_0\to{}U, and an indexed family of maps D_1: \Pi_{(i,j:\Gamma_0)}\Pi_{(e:\Gamma_1(i,j))}~D_0(i)\to{}D_0(j). Any type X determines a diagram \Delta(X) on \Gamma. A cone on D with vertex X is then simply a morphism of diagram \Delta(X)\to{} D. By functoriality of \Delta, we get for each f: Y\to X a map \Delta(f):\Delta(Y)\to\Delta(X), and pre-composing by \Delta(f) gives an operation from cones with vertex X to cones with vertex Y. A cone with vertex X is said to be limiting if for each f : Y\to X, this precomposition map is an equivalence. A limiting cone always exists, since we can take the type \mathsf{limit}(D) to be the type of pairs (x,h), where

x:\Pi_{(i:\Gamma_0)}~D_0(i)
h : \Pi_{(i,j:\Gamma_0)}\Pi_{(e:\Gamma_1(i,j))}~D_1(e,x_i)=x_j.

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 (x,h),(y,k):\mathsf{limit}(D), the identity type (x,h)=(y,k) is equivalent to the limit of the diagram I(D) over \Gamma, defined by

I(D)_0(i) := (x_i=y_i)
I(D)_1(e,p) := h_e^{-1}\cdot \mathsf{ap}_{D_1(e)}(p)\cdot k_e.


Identity types of coinductive types

Using the previous lemma, we can characterize the identity type of the coinductive type \mathsf{M}(A,B) in a useful way:

Theorem 2. Let (A,B) be an indexed container, and let (x,h),(y,k):\mathsf{M}(A,B). Then the following are equivalent types:

  1. The type (x,h)=(y,k).
  2. The type of pairs (\alpha,\beta) consisting of \alpha:\mathsf{destr}_0(x,h)=\mathsf{destr}_0(y,k) and \beta:\Pi_{(z:B(\mathsf{destr}_0(x,h)))}~\mathsf{destr}_1((x,h),z)=\mathsf{destr}_1((y,k),\mathsf{trans}(\alpha,z)). Here \mathsf{destr}_0 and \mathsf{destr}_1 are the first and second component of the map \mathsf{destr}_{A,B}:\mathsf{M}(A,B)\to{}P_{A,B}(\mathsf{M}(A,B)).
  3. The limit of the type sequence
    \cdots \longrightarrow{}(x_2=y_2) \longrightarrow (x_1=y_1)\longrightarrow{}(x_0=y_0),
    where the maps v_n:(x_{n+1}=y_{n+1})\to{}(x_n=y_n) are given by v_n(p):=h_n^{-1}\cdot\mathsf{ap}_{u_n}(p)\cdot k_n.

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 C=(I,A,B,k) consists of a type I, a type family A : I\to{}U, a further type family B:\Pi_{(i:I)}~(A(i)\to{}U), and a re-indexing function k : \Pi_{(i:I)}\Pi_{(a:A(i))} (B(i)\to{}I). Just like ordinary containers, an indexed container C determines a polynomial endofunctor acting on the category U^I. It is defined by

P_C(X)(i) := \Sigma_{(a:A(i))}\Pi_{(b:B(i))}~X(k(b)).

Again, the functorial action of P_C is given by precomposition. As with ordinary containters, one can construct the final coalgebra for P_C  as the limit of the type sequence

\cdots \longrightarrow{} P_C^2({-}\mapsto{}\mathbf{1})(i) \longrightarrow{} P_C({-}\mapsto{}\mathbf{1})(i) \longrightarrow{} \mathbf{1}.

Here, {-}\mapsto\mathbf{1} indicates the constant type family over I with value \mathbf{1}.

Our goal is to define an indexed container (I,A',B',k) that defines the bisimilation relation \mathsf{Bisim}_{A,B} : \mathsf{M}(A,B)\to{}\mathsf{M}(A,B)\to{} U as a coinductive type. Note that we can basically read off from the second equivalent description of the identity type of \mathsf{M}(A,B) in Theorem 2 what A' and B' should be:

  • For the indexing type we take I:=\mathsf{M}(A,B)\times{}\mathsf{M}(A,B).
  • We define A'(i,j) := \mathsf{destr}_0(i)=\mathsf{destr}_0(j).
  • We define B'(i,j,p) := B(\mathsf{destr}_0(i)).
  • We define the re-indexing function k by k(i,j,p,b) := (\mathsf{destr}_1(i,b),\mathsf{destr}_1(j,\mathsf{trans}(p,b)).

Now let us compute the action of the polynomial functor P_C explicitly. We have

P_C(X)(i,j) := \Sigma_{(p:\mathsf{destr}_0(i)=\mathsf{destr}_0(j))}\Pi_{(b:B(\mathsf{destr}_0(i)))}~X(\mathsf{destr}_1(i,z),\mathsf{destr}_1(j,\mathsf{trans}(p,z)).

Note that the third description in Theorem 2 already states that the type family (i,j:M(A,B)) \mapsto (i=j) is a coalgebra for latex P_C. 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 \mathsf{Bisim}_{A,B}(i,j), and the type sequence of Theorem 2. In other words, one has to show that we have a diagram of the form

nat_equiv

Update 10/17/2016: Included an explicit description of the coalgebra structure of M(A,B).

Advertisements

One thought on “What I learned this summer about coinductive types

  1. Pingback: Formalizing the graph model of type theory, part 3 | Egbert RIJKE

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