# Does co-inductive and co-recursive types also have their recursors?

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.

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.
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.