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 hiding (_+_)
open import Two
open import SetsAndFunctions


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

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

P : ℕ∞  𝟙 + ℕ∞
P u = two-cases Zero' (Pred' u) (positivity u)

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₀ : positivity u    S(P u)  u
  lemma₀ r = trans claim₁ (sym(isZero-equal-Zero r))
    where 
     claim₀ : P u  Zero'
     claim₀ = cong (two-cases Zero' (Pred' u)) r
     claim₁ : S(P u)  Zero
     claim₁ = cong S claim₀
  lemma₁ : positivity u    S(P u)  u
  lemma₁ r = trans claim₁ (sym claim₃)
   where  
     claim₀ : P u  Pred' u
     claim₀ = cong (two-cases Zero' (Pred' u)) r
     claim₁ : S(P u)  Succ(Pred u)
     claim₁ = cong S claim₀
     claim₂ : u  Zero
     claim₂ s = Lemma[b≡₀→b≢₁](cong positivity 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 = 
 funext 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 = 
 funext  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 (funext 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(funext 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(funext(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 = funext 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}