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.

someco-dependent objects coexisting with an otherwise standard type-theoretic foundation. $\endgroup$