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

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

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

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

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