Codependent types in type theory

Question

The nLab's article on coinductive types here states that

There is an obstacle to the complete dualization of the usual rules for inductive types in homotopy type theory, including dualizing the induction principle to a “coinduction principle”. For this some form of “codependent types” would be needed.

How would one go about defining such a codependent type in type theory?

Answer 1

Here is how I would go to dualize the induction principle into a sort of coinduction principle, leading to a sort of codependent type.

An inductive type $C$ is defined with a list of constructors $c_i$, and the principle that for each type $X$ with constructors $x_i$ that can be "interpreted as a realization of $C$ and the $c_i$'s", there is a destructor $d_C^X:C\to X$ that computes by substituting, in a term $c:C$, the $x_i$'s for the $c_i$'s (see hereafter for conditions of interpretability). From this constructors-realization principle, you can derive:

• the recursion principle by taking $X$ in the form $C\times B$;
• the induction principle by taking a type family $B:C\to U$ and $X$ in the form $\sum_{c:C}B(c)$.

Let's take $\mathbb{N}$ and its 2 constructors $0:\mathbb{N}$ and $s:\mathbb{N}\to\mathbb{N}$ as an example. Given a type family $P:\mathbb{N}\to U$, with $0_P:P(0)$ and $s_P:\prod_{n:\mathbb{N}}(P(n)\to P(s(n)))$, we can define $0'=(0,0_P)$ and $s':(\sum_{n:\mathbb{N}}P(n))\to(\sum_{n:\mathbb{N}}P(n))$ so that $s'((n,p))=(s(n),s_P(n)(p))$. The corresponding destructor is $d:\mathbb{N}\to\sum_{n:\mathbb{N}}P(n)$, whose first projection is the $\mathbb{N}$ identity and the second projection has type $\prod_{n:\mathbb{N}}P(pr_1(d(n)))$ which is equivalent to $\prod_{n:\mathbb{N}}P(n)$.

This constructors-realization principle dualizes naturally into a destructors-realization principle for coinductive types:

Indeed, a coinductive type $D$ is defined with a list of destructors $d_i$ and the principle that for each type $X$ with destructors $x_i$ that can be "interpreted as a realization of $D$ and the $d_i$'s", there is a constructor $c_X^D:X\to D$ so that $d_i(c_X^D(x),\Delta_i)$ computes as either $x_i(x,\Delta_i)$ when the codomain of $d_i$ is not $D$, or as $c_X^D(x_i(x, \Delta_i))$ when the codomain of $d_i$ is $D$ (see hereafter for conditions of interpretability).

From this destructors-realization principle you can derive:

• the corecursion principle by taking a type $X$ in the form $D\times B$;
• some sort of coinduction principle, by taking a type family $B:D\to U$ and $X$ in the form $\sum_{d:D}B(d)$. The types of $c_{\sum_{d:D}B(d)}^D$ and the $x_i$'s in the form $(\sum_{d:D}B(d))\to D$ can be rewritten as $\prod_{d:D}(B(d)\to D)$, which gives you some form of "codependent type".

---

There are conditions on the $c_i$'s, $d_i$'s and $x_i$'s so that $X$ and the $x_i$'s can be "interpreted as a realization of $C$ and the $c_i$'s", or of "$D$ and the $d_i$'s". Noting $C_i$ (respectively $D_i$, $X_i$) the type of $c_i$ (respectively $d_i$, $x_i$), we have:

• For inductive types, $X_i$ shall match the type obtained by substituting $X$ for $C$ in $C_i$; moreover, $C_i$ shall satisfy the classical strict positivity condition to prevent any possible occurence of a destructor $d_C^Y$ in a term $c:C$. Indeed, knowing the $x_i$'s we can interpret the $c_i$'s, but can't in general interpret a destructor $d_C^Y$ in a consistent way: the constructors-realization principle is a way to explain the reason for the strict positivity condition.
• For coinductive types, $X_i$ shall match the type obtained by partially substituting $X$ for $D$ in the first variable type and in the codomain of $D_i$. The first variable shall be of type $D$, so that $d_i$ is a destructor, while the codomain shall be either $D$ or have no occurence of $D$, so that we know how to compute $d_i(c_X^D(x),\Delta_i)$ (see above). The second to last $x_i$ variables types shall match the corresponding $d_i$ variables types; they may contain occurences of $D$ without restriction.