Co-induction principle

Question

It's known that Nat-ind = Nat-rec ⨯ Nat-initiality

Has someone figured out how to define a suitable Conat-coind such that Conat-coind = Conat-corec ⨯ Conat-finality?

It it a plausible thing to do?

Do we need some notion of co-dependent types?

EDIT: Here are the definitions of Nat-ind, Nat-rec, Nat-initiality:

Nat-ind ≔  (ind : (A : ℕ → 𝕌) (a₀ : A 0) (a₁ : (x : ℕ) → A x → A (S x)) (x : ℕ) → A x) 
         ⨯ (ind-0 : (A : ℕ → 𝕌) (a₀ : A 0) (a₁ : (x : ℕ) → A x → A (S x)) → ind A a₀ a₁ 0 ≡ a₀)
         ⨯ (ind-1 : (A : ℕ → 𝕌) (a₀ : A 0) (a₁ : (x : ℕ) → A x → A (S x)) (x : ℕ) 
                           → 
                    ind A a₀ a₁ (S x) ≡ a₁ x (ind A a₀ a₁ x)
           )
         ⨯ ()

Nat-rec ≔ (rec : (A : 𝕌) (a₀ : A) (a₁ : A → A) → (ℕ → A))
        ⨯ (rec-0 : (A : 𝕌) (a₀ : A) (a₁ : A → A) → rec A a₀ a₁ 0 ≡ a₀)
        ⨯ (rec-1 : (A : 𝕌) (a₀ : A) (a₁ : A → A) (x : ℕ) → rec A a₀ a₁ (S x) ≡ a₁ (rec A a₀ a₁ x))
        ⨯ ()

Nat-initiality : (A : 𝕌) (a₀ : A) (a₁ : A → A) (f : ℕ → A) 
                 (f-0 : f 0 ≡ a₀) 
                 (f-1 : (x : ℕ) → f (S x) ≡ a₁ (f x))
                 →
                 f ≡ rec A a₀ a₁

By this Nat-ind = Nat-rec ⨯ Nat-initiality I, of course, mean isomorphism/equivalence:

Nat-ind ≃ Nat-rec ⨯ Nat-initiality

So paraphrasing my original question: is it possible to come up with such a type Conat-coind (a co-induction principle) such that Conat-coind ≃ Conat-corec ⨯ Conat-finality. Of course there is the trivial identity-equivalence solution. But that's not what I am looking for.

Answer 1

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 (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 corec/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 0 and S are just a roundabout way of spelling out refl. 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 (hd, tl, 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.