It it a plausible thing to do?
I could just be lacking imagination, but this doesn't seem like a plausible thing to do. This seems to be a misguided attempt at understanding coinduction by duality with induction. So I'm going to answer this more general question instead:
What is the dual of induction?
I will convince you that the answer is indeed that the dual of induction, aka. "coinduction", is the bisimilarity principle, "bisimilarity is equality" (copied below from your previous question):
R : Stream A → Stream A → 𝕌
R-head : (xs ys : Stream A) → R xs ys → xs.head ≡ ys.head
R-tail : (xs ys : Stream A) → R xs ys → R xs.tail ys.tail
bisim : (xs ys : Stream A) → R xs ys → xs ≡ ys
My answer to your previous question gives a weak justification: given a
corec : (A -> B * A) -> A -> Stream B, the bisimilarity principle is equivalent to the uniqueness of
corec, like how induction is equivalent to the uniqueness of
rec : (1 + A -> A) -> Nat -> A.
You did not find that satisfactory because with dependent types, induction also gives you a definition of
rec is just a non-dependent specialization of induction). So you went looking for something similar with coinductive types, i.e., a
coind with which you can define
corec. But I think that is asking too much. I can't even begin to imagine what that would look like. I'd be happy to be proven wrong.
At least one particularity that distinguishes the bisimilarity principle and induction among all other equivalent properties is that they don't mention
rec. But beyond that there doesn't seem to be much symmetry between the bisimilarity principle and induction that one usually expects from "duals".
An important idea towards a stronger justification is that types are groupoids. A type should be thought of as not just a set of values, the "equality" relation between values is also part of the structure of a type.
So when you define a type's constructors/destructors, you are also defining constructors/destructors for its equality type (aka. path type).
0 : 0 = 0
S : n = m -> S n = S m
rec : R 0 0 -> ((n m : Nat) -> R n m -> R (S n) (S m)) -> (n m : Nat) -> n = m -> R n m
For a simple inductive type like
Nat, the constructors are kinda boring because
S are just a roundabout way of spelling out
rec (the non-dependent eliminator for equality on
Nat) is slightly more interesting: it's just induction, parameterized by a binary predicate instead of a unary predicate! Induction over
Nat is (a consequence of) recursion over its path type viewed as another inductive type.
Same thing for streams (
corec). Equality on
Stream becomes a coinductive type, whose
corec is just the bisimilarity principle!
hd : x = y -> hd x = hd y
tl : x = y -> tl x = tl y
corec : ((x y : Stream A) -> R x y -> (hd x = hd y) /\ (R (tl x) (tl y))) -> (x y : Stream A) R x y -> x = y
There you have it. When types are groupoids:
- Induction is elimination of equality for inductive types.
- Coinduction is introduction of equality for coinductive types.