# Is there a notion of “codependent” types for coinductive types?

Inductively defined types are common within the type theory literature, and there are many ways of characterizing them. In the Homotopy Type Theory book, inductive types are characterized using certain "induction principles" describing how to construct (dependent) maps out of or into such types. Thus, in some sense, we can construct inductive types from dependent types.

My question is: Is there some characterization of coinductive types that is dual to this "induction principle" characterization of inductive types? Moreover, if this is the case, does this notion still rely on the standard notion of dependent types (with the role of dependent sum and dependent product swapped, I suppose), or some new notion of "codependent types"?

There is a dual notion of coinductive types, yes, and we don't need to look past the framework of dependent types. One way to think about inductive types is as initial algebras. In this perspective, the defining data for an inductive type is a functor $F : \operatorname{Type} \to \operatorname{Type}$ of a particular form, and an $F$-algebra is a type $A$ together with a natural transformation $F A \to A$. All the data for the inductive type you wish to define (the type itself, its recursion rule, and its computation rules) is then equivalent to the type of initial $F$-algebras. Dually, the coinductive type should be the type of terminal $F$-coalgebras.

You can see Section 5.4 in the HoTT book for details (as least for the inductive case), but it will be helpful to see an example. Consider the inductive definition of the natural numbers:

Inductive Nat : Type :=
| zero : Nat
| succ : Nat -> Nat


Directly from this definition, you can read off a particular functor: \begin{align*} F := \lambda A : \operatorname{Type} \mathop{.} 1 + A \end{align*} Think of the arguments to $+$ as the data you need to provide to the "zero" constructor and the "succ" constructor, respectively, replacing Nat by the type parameter $A$ when it occurs. From here, we can define what it means for a type to have an $F$ algebra and $F$ coalgebra structure: \begin{align*} \operatorname{FAlgebra} &:= \lambda A : \operatorname{Type} \mathop{.} F A \to A \\ \operatorname{FCoalgebra} &:= \lambda A : \operatorname{Type} \mathop{.} A \to F A \end{align*} An $F$ algebra structure on a type $A$ is familiar: it consists just of the data you need to inductively define a function from $\operatorname{Nat} \to A$. (To see why, remember that a function $1 + A \to A$ consists equivalently of a function $1 \to A$ together with a function $A \to A$. These are the base case and inductive case for the inductive definition, respectively.) Following that intuition, the natural numbers are then just an $F$-algebra $\operatorname{Nat}$ with the property that there is a unique homomorphism (that is, a map preserving the $F$-algebra structure in a suitable sense) from $\operatorname{Nat}$ to any other $F$-algebra. That is, $\operatorname{Nat}$ is the initial $F$-algebra.

The coinductive case is dual. An $F$-coalgebra structure on $A$ is the data necessary to define a function from $A$ to a type built from zero and succ: for any element of $A$, think of the corresponding element you build in $1 + A$ to be deciding whether that element maps to zero or a successor and, if it maps to a successor, what it is the successor of. The target type of this construction is the corresponding coinductive type: the terminal $F$ coalgebra is an $F$ coalgebra called $\operatorname{CoNat}$ with the property that there is a unique $F$-coalgebra homomorphism from any $F$ colagebra to $\operatorname{CoNat}$.

Bonus: you didn't ask about the possibility of "higher" coinductive types, but I should say something about them anyway. The HoTT book doesn't talk about them as far as I know, and they seem a bit delicate.

To be concrete, consider the following higher inductive definition:

Inductive Foo : Type :=
| zero : Foo
| succ : Foo -> Foo
| succ_path : forall x:Foo, succ x = x


This definition should let us build terms in Foo out of zero and successor, as for the natural numbers, but should also let us uniformly prove that every Foo is equal to its successor. In order to get a function from Foo to some type $A$, you ought to provide a base case $z : A$, inductive case $s : A \to A$, and a proof that $s a = a$ for all $a$. With that in mind, we at least know what it should mean to be an algebra: \begin{align*} \operatorname{FooAlgebra} A = \sum_{z : A} \sum_{s : A \to A} \prod_{a:A} s a = a \end{align*}

If we want to see what a coalgebra should be, one approach would be to find a functor $F : \operatorname{Type} \to \operatorname{Type}$ such that the type $F A \to A$ is equivalent to $\operatorname{FooAlgebra} A$, and look at coalgebras of that functor. I'm not sure how plausible it is to find such a functor, however. Even without it, though, it may (or may not) be possible to give an independent account of what the coalgebras should look like. I don't know what work has been done in this area.

• Wow, thank you for the in-depth response! However, still I wonder: Is the condition that a (co)inductive type be initial (final) what is characterized in the HoTT book by the so called "Induction principles" -- and hence dependent types? I believe the book mentions that these principles are related to categorical semantics, but doesn't go into further detail than that (from what I've read so far). – Nathan BeDell Jan 25 '17 at 22:12
• The equivalence between universal properties and induction principles is discussed in chapter 5 of the HoTT Book. – Mike Shulman Jan 26 '17 at 20:05