I'm new to type theory, and recently read introductory materials where dependent type are discussed. One of my friend asked me, "Those dependent types are having recursors & 'inductors'(dependent eliminators), but how about those types that is co-inductive/co-recursive?"
Some related example is much appreciated.
To understand coinduction, it helps to understand the categorical presentation of induction (since, as far as I know, coinduction comes from dualizing it there).
The idea behind induction is that we have a functor $F : C → C$, and we consider algebras $(A,\ α : F A → A)$. The operation $α$ specifies how to interpret the structure given by $F$ into $A$. Then, an inductively defined type is an initial algebra $(μF, \mathsf{in} : F μF → μF)$, which mean there is a unique homomorphism $\mathsf{fold}_A : μF → A$ to any other algebra. This homomorphism is the recursor, and the uniqueness allows us to define the induction principle in various ways, depending on the setting.
Coinduction flips most of these arrows around. Instead of algebras, we have coalgebras, $(A, α : A → F A)$. And instead of being initial, the coinductively defined type is final, so we get a unique $unfold_A : A → νF$ from any other coalgebra. So, instead of a recursive way of "eliminating", we get a recursive way of "introducing," and the eliminators are non-recursive.
However this flipping around makes some thing not work quite as nicely with coinductive types. I have an Agda development here that tries to explain the stuff about induction above in more detail, with the idea of finding something similar for coinduction. But I never got around to figuring that part out. And as far as I know, there is no known 'nice' interpretation of the coinductive case similar to the inductive one. The one thing to note is that 'just do the same thing with slices as induction' turns out to be uninteresting for coinduction.
One promising thing I have seen is that in cubical type theory, definition by coinduction gives a natural way of showing that two values of a coinductive type are equal, because it automatically corresponds to bisimulation, which is the usual notion of equality for coinductive things. The idea is that an identity from $x : A$ to $y : A$ is a function $eq : \mathbb{I} \to A$ (where $\mathbb{I}$ is an 'interval' type with distinguished values $0$ and $1$) such that $eq\; 0$ evaluates to $x$ and $eq \; 1$ evaluates to $y$. Then $unfold_\mathbb{I}$ gives us a principle for proving $x = y : νF$ by breaking things down to individual pieces like $\mathsf{step} : \mathbb{I} \to F\ \mathbb{I}$. You can see an example of this here.
I don't know if that completely answers your question or not. Hopefully it helps some.
