Martin Escardo 2012.

We investigate coinduction and corecursion on ℕ∞, the generic
convergent sequence.

We show that set ℕ∞ satisfies the following universal property for a
suitable P : ℕ∞ → ① + ℕ∞, where ① is the singleton type
with an element *.

For every set X and every p : X → ① + X there is a unique h : X → ℕ∞
such that
p
X ------------------> ① + X
|                       |
|                       |
h  |                       | ① + h
|                       |
|                       |
v                       v
ℕ∞ -----------------> ① + ℕ∞
P

The maps p and P are called coalgebras for the functor ① + (-), and
the above diagram says that h is a coalgebra morphism from p to P.

In equational form, this is

P ∘ h ≡ (① + h) ∘ p,

which can be considered as a corecursive definition of h.  The map P
(a sort of predecessor function) is an isomorphism with inverse S (a
sort of successor function). This follows from Lambek's Lemma once the
above universal property is established, but we actually need to know
this first in order to prove the universal property.

S : ① + ℕ∞ → ℕ∞
S(in₀ *) = Zero
S(in₁ u) = Succ u

Using this fact, the above corecursive definition of h is equivalent
to:

h ≡ S ∘ (① + h) ∘ p

or

h(x) ≡ S((① + h)(p x)).

Now p x is either of the form in₀ * or in₁ x' for a unique x' : X, and
hence the above equation amounts to

h(x) ≡ Zero,           if p x ≡ in₀ *,
h(x) ≡ Succ(h x'),     if p x ≡ in₁ x',

once we know the definition of ① + h. This shows more clearly how the
diagram can be considered as a (co)recursive definition of h, and
indicates how h may be constructed.

In order to show that any two functions that make the above diagram
commute are unique, that is, that the above two conditional equations
uniquely determine h, we develop a coinduction principle based on
bisimulations. This gives a technique for establishing equalities on
ℕ∞.

\begin{code}

{-# OPTIONS --without-K #-}

module CoNaturals where

open import GenericConvergentSequence
open import CurryHoward
open import Equality
open import Extensionality
open import Naturals
open import Two
open import SetsAndFunctions

Zero' : ① + ℕ∞
Zero' = in₀ *

Pred' : ℕ∞ → ① + ℕ∞
Pred' u = in₁(Pred u)

P : ℕ∞ → ① + ℕ∞
P u = two-cases Zero' (Pred' u) (incl u 0)

P-Zero : P Zero ≡ Zero'
P-Zero = refl

P-Succ : ∀(u : ℕ∞) → P(Succ u) ≡ in₁ u
P-Succ u = cong in₁ Pred-Succ-u-is-u

S : ① + ℕ∞ → ℕ∞
S(in₀ *) = Zero
S(in₁ u) = Succ u

P-S-id : ∀{y : ① + ℕ∞} → P(S y) ≡ y
P-S-id{in₀ *} = refl
P-S-id{in₁ u} = refl

S-injective : ∀{y z : ① + ℕ∞} → S y ≡ S z → y ≡ z
S-injective r = trans (sym P-S-id) (trans(cong P r) P-S-id)

S-P-id : ∀{u : ℕ∞} → S(P u) ≡ u
S-P-id {u} = two-equality-cases lemma₀ lemma₁
where
lemma₀ : incl u 0 ≡ ₀ → S(P u) ≡ u
lemma₀ r = trans claim₁ (sym(isZero-equal-Zero r))
where
claim₀ : P u ≡ Zero'
claim₀ = cong (λ b → two-cases Zero' (Pred' u) b) r
claim₁ : S(P u) ≡ Zero
claim₁ = cong S claim₀
lemma₁ : incl u 0 ≡ ₁ → S(P u) ≡ u
lemma₁ r = trans claim₁ (sym claim₃)
where
claim₀ : P u ≡ Pred' u
claim₀ = cong (λ b → two-cases Zero' (Pred' u) b) r
claim₁ : S(P u) ≡ Succ(Pred u)
claim₁ = cong S claim₀
claim₂ : u ≠ Zero
claim₂ s = Lemma[b≡₀→b≠₁](cong (λ v → incl v 0) s) r
claim₃ : u ≡ Succ(Pred u)
claim₃ = not-Zero-is-Succ claim₂

P-injective : ∀{u v : ℕ∞} → P u ≡ P v → u ≡ v
P-injective r = trans (sym S-P-id) (trans(cong S r) S-P-id)

①+ : {X Y : Set} → (X → Y) → ① + X → ① + Y
①+ f (in₀ s) = in₀ s
①+ f (in₁ x) = in₁(f x)

alg-mophism-remark₀ : {X : Set} → ∀(p : X → ① + X) → ∀(h : X → ℕ∞) →

P ∘ h ≡ (①+ h) ∘ p  →  h ≡ S ∘ (①+ h) ∘ p

alg-mophism-remark₀ p h a =
extensionality(λ x → trans (sym S-P-id) (cong (λ F → S(F x)) a))

alg-mophism-remark₁ : {X : Set} → ∀(p : X → ① + X) → ∀(h : X → ℕ∞) →

h ≡ S ∘ (①+ h) ∘ p  →  P ∘ h ≡ (①+ h) ∘ p

alg-mophism-remark₁ p h b =
extensionality (λ x → trans (cong (λ G → P(G x)) b) P-S-id)

diagram-commutes : {X : Set} → (X → ① + X) → (X → ℕ∞) → Prp
diagram-commutes p h = (P ∘ h ≡ (①+ h) ∘ p)

homomorphism-existence : {X : Set} →

∀(p : X → ① + X) → ∃ \(h : X → ℕ∞) → diagram-commutes p h

homomorphism-existence {X} p = ∃-intro h (extensionality h-spec)
where
q : ① + X → ① + X
q(in₀ s) = in₀ s
q(in₁ x) = p x

Q : ℕ → ① + X → ① + X
Q 0 z = z
Q(succ n) z = q(Q n z)

E : ① + X → ₂
E(in₀ s) = ₀
E(in₁ x) = ₁

h-lemma : ∀ z → E(q z) ≡ ₁ → E z ≡ ₁
h-lemma (in₀ s) r = r
h-lemma (in₁ x) r = refl

h : X → ℕ∞
h x = ((λ i → E(Q(succ i) (in₁ x))) ,
λ i → h-lemma(Q(succ i) (in₁ x)))

h-spec : ∀ x → P(h x) ≡ (①+ h)(p x)
h-spec x = equality-cases (p x) lemma₀ lemma₁
where
lemma₀ : ∀(s : ①) → p x ≡ in₀ s → P(h x) ≡ (①+ h)(p x)
lemma₀ * r = trans claim₂ (sym claim₀)
where
claim₀ : (①+ h)(p x) ≡ Zero'
claim₀ = cong (①+ h) r
claim₁ : h x ≡ Zero
claim₁ = isZero-equal-Zero(cong E r)
claim₂ : P(h x) ≡ Zero'
claim₂ = trans (cong P claim₁) P-Zero

lemma₁ : ∀(x' : X) → p x ≡ in₁ x' → P(h x) ≡ (①+ h)(p x)
lemma₁ x' r = trans claim₆ (sym claim₀)
where
claim₀ : (①+ h)(p x) ≡ in₁(h x')
claim₀ = cong (①+ h) r
claim₁ : ∀ n → q(Q n (in₁ x)) ≡ Q n (p x)
claim₁ 0 = refl
claim₁ (succ n) = cong q (claim₁ n)
claim₂ : ∀ n → q(Q n (in₁ x)) ≡ Q n (in₁ x')
claim₂ n = trans (claim₁ n) (cong (Q n) r)
claim₃ : ∀ n → E(q(Q n (in₁ x))) ≡ E(Q n (in₁ x'))
claim₃ n = cong E (claim₂ n)
claim₄ : ∀ i → incl(h x) i ≡ incl(Succ(h x')) i
claim₄ 0  = claim₃ 0
claim₄ (succ i) = claim₃(succ i)
claim₅ : h x ≡ Succ(h x')
claim₅ = incl-mono(extensionality claim₄)
claim₆ : P(h x) ≡ in₁(h x')
claim₆ = cong P claim₅

ℕ∞-corec  : {X : Set} → (X → ① + X) → (X → ℕ∞)
ℕ∞-corec p = ∃-witness(homomorphism-existence p)

\end{code}

We now discuss coinduction. We first define bisimulations.

\begin{code}

ℕ∞-bisimulation : (ℕ∞ → ℕ∞ → Prp) → Prp
ℕ∞-bisimulation R =
∀ u v → R u v → positivity u ≡ positivity v  ∧  R(Pred u)(Pred v)

ℕ∞-coinduction : ∀(R : ℕ∞ → ℕ∞ → Prp) → ℕ∞-bisimulation R →

∀ u v → R u v → u ≡ v

ℕ∞-coinduction R b u v r = incl-mono(extensionality(lemma u v r))
where
lemma : ∀ u v → R u v → ∀ i → incl u i ≡ incl v i
lemma u v r 0 =  ∧-elim₀(b u v r)
lemma u v r (succ i) = lemma (Pred u) (Pred v) (∧-elim₁(b u v r)) i

\end{code}

To be able to use it for our purpose, we need to investigate
coalgebra homomorphisms in more detail.

\begin{code}

alg-morphism-Zero : {X : Set} →

∀(p : X →  ① + X) → ∀(h : X → ℕ∞) → diagram-commutes p h

→ ∀(x : X) → ∀(s : ①) → p x ≡ in₀ s → h x ≡ Zero

alg-morphism-Zero p h a x * c = trans (sym S-P-id) (cong S claim₃)
where
claim₁ : P(h x) ≡ (①+ h)(p x)
claim₁ = cong (λ t → t x) a
claim₂ : (①+ h)(p x) ≡ Zero'
claim₂ = cong (①+ h) c
claim₃ : P(h x) ≡ in₀ *
claim₃ = trans claim₁ claim₂

alg-morphism-Succ : {X : Set} →

∀(p : X →  ① + X) → ∀(h : X → ℕ∞) → diagram-commutes p h

→ ∀(x : X) → ∀(x' : X) → p x ≡ in₁ x' → h x ≡ Succ(h x')

alg-morphism-Succ p h a x x' c = trans (sym S-P-id) (cong S claim₃)
where
claim₁ : P(h x) ≡ (①+ h)(p x)
claim₁ = cong (λ t → t x) a
claim₂ : (①+ h)(p x) ≡ in₁(h x')
claim₂ = cong (①+ h) c
claim₃ : P(h x) ≡ in₁(h x')
claim₃ = trans claim₁ claim₂

\end{code}

The following two technical lemmas will be used to construct a
bisimulation later:

\begin{code}

alg-morphism-positivity : {X : Set} →

∀(p : X →  ① + X) → ∀(f g : X → ℕ∞)

→ diagram-commutes p f → diagram-commutes p g

→ ∀(x : X) → positivity(f x) ≡ positivity(g x)

alg-morphism-positivity {X} p f g a b x =
equality-cases (p x) lemma₀ lemma₁
where
lemma₀ : ∀(s : ①) → p x ≡ in₀ s → positivity(f x) ≡ positivity(g x)
lemma₀ s c = trans f-lemma (sym g-lemma)
where
f-lemma : positivity(f x) ≡ ₀
f-lemma = cong positivity(alg-morphism-Zero p f a x s c)
g-lemma : positivity(g x) ≡ ₀
g-lemma = cong positivity(alg-morphism-Zero p g b x s c)

lemma₁ : ∀(x' : X) → p x ≡ in₁ x' → positivity(f x) ≡ positivity(g x)
lemma₁ x' c = trans f-lemma (sym g-lemma)
where
f-lemma : positivity(f x) ≡ ₁
f-lemma = cong positivity(alg-morphism-Succ p f a x x' c)
g-lemma : positivity(g x) ≡ ₁
g-lemma = cong positivity(alg-morphism-Succ p g b x x' c)

alg-morphism-Pred : {X : Set} →

∀(p : X →  ① + X) → ∀(f g : X → ℕ∞)

→ diagram-commutes p f → diagram-commutes p g

→ ∀ x u v → u ≡ f x → v ≡ g x

→ ∃ \x' → Pred u ≡ f x'  ∧  Pred v ≡ g x'

alg-morphism-Pred {X} p f g a b x u v d e =
equality-cases (p x) lemma₀ lemma₁
where
lemma₀ : ∀(s : ①) → p x ≡ in₀ s → ∃ \x' → Pred u ≡ f x' ∧  Pred v ≡ g x'
lemma₀ s c = ∃-intro x (∧-intro (lemma f a u d) (lemma g b v e))
where
lemma : ∀(h : X → ℕ∞) → P ∘ h ≡ (①+ h) ∘ p
→ ∀ u → u ≡ h x → Pred u ≡ h x
lemma h a u d = trans claim₁ (sym claim₀)
where
claim₀ : h x ≡ Zero
claim₀ = alg-morphism-Zero p h a x s c
claim₁ : Pred u ≡ Zero
claim₁ = cong Pred(trans d claim₀)

lemma₁ : ∀(x' : X) → p x ≡ in₁ x' → ∃ \x' → Pred u ≡ f x' ∧  Pred v ≡ g x'
lemma₁ x' c = ∃-intro x' (∧-intro (lemma f a u d ) (lemma g b v e ))
where
lemma :  ∀(h : X → ℕ∞) → P ∘ h ≡ (①+ h) ∘ p
→ ∀ u → u ≡ h x → Pred u ≡ h x'
lemma h a u d = trans (cong Pred d) lemma'
where
lemma' : Pred(h x) ≡ h x'
lemma' = cong Pred(alg-morphism-Succ p h a x x' c)

\end{code}

We are finally able to prove the uniqueness of coalgebra homomorphisms
from p to P.

\begin{code}

homomorphism-uniqueness : {X : Set} →

∀(p : X → ① + X) → ∀(f g : X → ℕ∞)

→ diagram-commutes p f → diagram-commutes p g

→ f ≡ g

homomorphism-uniqueness {X} p f g a b = extensionality lemma
where
R : ℕ∞ → ℕ∞ → Prp
R u v = ∃ \x → u ≡ f x  ∧  v ≡ g x

r : ∀ x → R(f x)(g x)
r x = (x , refl , refl)

R-positivity : ∀ u v → R u v → positivity u ≡ positivity v
R-positivity u v (x , c , d) =
trans (cong positivity c) (trans e (cong positivity (sym d)))
where
e : positivity(f x) ≡ positivity(g x)
e = alg-morphism-positivity {X} p f g a b x

R-Pred : ∀ u v → R u v → R(Pred u)(Pred v)
R-Pred u v (x , c , d) =
(∃-witness lemma , ∧-elim₀(∃-elim lemma) , ∧-elim₁(∃-elim lemma))
where
lemma : ∃ \x' → Pred u ≡ f x' ∧ Pred v ≡ g x'
lemma = alg-morphism-Pred p f g a b x u v c d

R-bisimulation : ℕ∞-bisimulation R
R-bisimulation u v r = ∧-intro (R-positivity u v r) (R-Pred u v r)

lemma : ∀ x → f x ≡ g x
lemma x = ℕ∞-coinduction R R-bisimulation (f x) (g x) (r x)

\end{code}

Putting existence and uniqueness together, we get that P is the final
coalgebra, as claimed:

\begin{code}

P-is-the-final-coalgebra : {X : Set} →

∀(p : X → ① + X) → ∃! \(h : X → ℕ∞) → diagram-commutes p h

P-is-the-final-coalgebra {X} p =
∧-intro(homomorphism-existence p)(homomorphism-uniqueness p)

\end{code}