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 --exact-split --safe #-}

module CoNaturals where

open import SpartanMLTT
open import Naturals
open import Two
open import GenericConvergentSequence

Zero' : 𝟙 + ℕ∞
Zero' = inl *

Pred' : ℕ∞  𝟙 + ℕ∞
Pred' u = inr(Pred u)

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

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

P-Succ : (u : ℕ∞)  P(Succ u)  inr u
P-Succ u = ap inr Pred-Succ-u-is-u

S : 𝟙 + ℕ∞  ℕ∞
S(inl *) = Zero
S(inr u) = Succ u

P-S-id : {y : 𝟙 + ℕ∞}  P(S y)  y
P-S-id{inl *} = refl
P-S-id{inr u} = refl

S-injective : {y z : 𝟙 + ℕ∞}  S y  S z  y  z
S-injective r = trans (sym P-S-id) (trans(ap 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₀ = ap (𝟚-cases Zero' (Pred' u)) r
     claim₁ : S(P u)  Zero
     claim₁ = ap S claim₀
  lemma₁ : positivity u    S(P u)  u
  lemma₁ r = trans claim₁ (sym claim₃)
   where  
     claim₀ : P u  Pred' u
     claim₀ = ap (𝟚-cases Zero' (Pred' u)) r
     claim₁ : S(P u)  Succ(Pred u)
     claim₁ = ap S claim₀
     claim₂ : u  Zero
     claim₂ s = Lemma[b≡₀→b≢₁](ap 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(ap S r) S-P-id)

𝟙+ : {X Y : U}  (X  Y)  𝟙 + X  𝟙 + Y
𝟙+ f (inl s) = inl s
𝟙+ f (inr x) = inr(f x)


alg-mophism-remark₀ : {X : U}  (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) (ap  F  S(F x)) a))
 where open import FunExt

alg-mophism-remark₁ : {X : U}  (p : X  𝟙 + X)  (h : X  ℕ∞)  

 h  S  (𝟙+ h)  p    P  h  (𝟙+ h)  p  

alg-mophism-remark₁ p h b = 
 funext  x  trans (ap  G  P(G x)) b) P-S-id)
 where open import FunExt


diagram-commutes : {X : U}  (X  𝟙 + X)  (X  ℕ∞)  U
diagram-commutes p h = (P  h  (𝟙+ h)  p)


homomorphism-existence : {X : U}  

 (p : X  𝟙 + X)  Σ \(h : X  ℕ∞)  diagram-commutes p h

homomorphism-existence {X} p = h , (funext h-spec)
 where
  open import FunExt

  q : 𝟙 + X  𝟙 + X
  q(inl s) = inl s
  q(inr x) = p x

  Q :   𝟙 + X  𝟙 + X
  Q 0 z = z
  Q(succ n) z = q(Q n z)

  E : 𝟙 + X  𝟚
  E(inl s) = 
  E(inr x) = 

  h-lemma : (z : 𝟙 + X)  E(q z)    E z  
  h-lemma (inl s) r = r
  h-lemma (inr x) r = refl
 
  h : X  ℕ∞
  h x = ((λ i  E(Q(succ i) (inr x))) , 
          λ i  h-lemma(Q(succ i) (inr x)))

  h-spec : (x : X)  P(h x)  (𝟙+ h)(p x)
  h-spec x = equality-cases (p x) lemma₀ lemma₁
   where 
    lemma₀ : (s : 𝟙)  p x  inl s  P(h x)  (𝟙+ h)(p x)
    lemma₀ * r = trans claim₂ (sym claim₀)
     where 
      claim₀ : (𝟙+ h)(p x)  Zero'
      claim₀ = ap (𝟙+ h) r
      claim₁ : h x  Zero
      claim₁ = isZero-equal-Zero(ap E r)
      claim₂ : P(h x)  Zero'
      claim₂ = trans (ap P claim₁) P-Zero

    lemma₁ : (x' : X)  p x  inr x'  P(h x)  (𝟙+ h)(p x)  
    lemma₁ x' r = trans claim₆ (sym claim₀)
     where 
      claim₀ : (𝟙+ h)(p x)  inr(h x')
      claim₀ = ap (𝟙+ h) r
      claim₁ : (n : )  q(Q n (inr x))  Q n (p x)
      claim₁ 0 = refl
      claim₁ (succ n) = ap q (claim₁ n)
      claim₂ : (n : )  q(Q n (inr x))  Q n (inr x')
      claim₂ n = trans (claim₁ n) (ap (Q n) r) 
      claim₃ : (n : )  E(q(Q n (inr x)))  E(Q n (inr x'))
      claim₃ n = ap 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₄) where open import FunExt

      claim₆ : P(h x)  inr(h x')
      claim₆ = ap P claim₅


ℕ∞-corec  : {X : U}  (X  𝟙 + X)  (X  ℕ∞) 
ℕ∞-corec p = pr₁(homomorphism-existence p)

\end{code}

We now discuss coinduction. We first define bisimulations.

\begin{code}


ℕ∞-bisimulation : (ℕ∞  ℕ∞  U)  U
ℕ∞-bisimulation R =
 (u v : ℕ∞)  R u v  positivity u  positivity v  ×  R(Pred u)(Pred v)


ℕ∞-coinduction : (R : ℕ∞  ℕ∞  U)  ℕ∞-bisimulation R  

  (u v : ℕ∞)  R u v  u  v

ℕ∞-coinduction R b u v r = incl-mono(funext(lemma u v r))
 where
  open import FunExt

  lemma : (u v : ℕ∞)  R u v  (i : )  incl u i  incl v i
  lemma u v r 0 =  pr₁(b u v r)
  lemma u v r (succ i) = lemma (Pred u) (Pred v) (pr₂(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 : U}  

    (p : X   𝟙 + X) (h : X  ℕ∞)  diagram-commutes p h

  (x : X) (s : 𝟙)  p x  inl s  h x  Zero
  
alg-morphism-Zero p h a x * c = trans (sym S-P-id) (ap S claim₃) 
 where
  claim₁ : P(h x)  (𝟙+ h)(p x) 
  claim₁ = ap  t  t x) a
  claim₂ : (𝟙+ h)(p x)  Zero'
  claim₂ = ap (𝟙+ h) c
  claim₃ : P(h x)  inl *
  claim₃ = trans claim₁ claim₂
 

alg-morphism-Succ : {X : U}  

    (p : X   𝟙 + X) (h : X  ℕ∞)  diagram-commutes p h

  (x x' : X)  p x  inr x'  h x  Succ(h x')
  
alg-morphism-Succ p h a x x' c = trans (sym S-P-id) (ap S claim₃) 
 where 
  claim₁ : P(h x)  (𝟙+ h)(p x)
  claim₁ = ap  t  t x) a
  claim₂ : (𝟙+ h)(p x)  inr(h x')
  claim₂ = ap (𝟙+ h) c
  claim₃ : P(h x)  inr(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 : U}  

    (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  inl s  positivity(f x)  positivity(g x)
  lemma₀ s c = trans f-lemma (sym g-lemma)
   where 
    f-lemma : positivity(f x)  
    f-lemma = ap positivity(alg-morphism-Zero p f a x s c)
    g-lemma : positivity(g x)  
    g-lemma = ap positivity(alg-morphism-Zero p g b x s c)

  lemma₁ : (x' : X)  p x  inr x'  positivity(f x)  positivity(g x)
  lemma₁ x' c = trans f-lemma (sym g-lemma)
   where
    f-lemma : positivity(f x)  
    f-lemma = ap positivity(alg-morphism-Succ p f a x x' c)
    g-lemma : positivity(g x)  
    g-lemma = ap positivity(alg-morphism-Succ p g b x x' c)


alg-morphism-Pred : {X : U}  

    (p : X   𝟙 + X) (f g : X  ℕ∞) 

  diagram-commutes p f  diagram-commutes p g

  (x : X) (u v : ℕ∞)  u  f x  v  g x

  Σ \(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  inl s  Σ \x'  Pred u  f x' ×  Pred v  g x' 
  lemma₀ s c = x , ((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₁ = ap Pred(trans d claim₀)

  lemma₁ : (x' : X)  p x  inr x'  Σ \x'  Pred u  f x' ×  Pred v  g x' 
  lemma₁ x' c = x' , ((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 (ap Pred d) lemma'
     where
      lemma' : Pred(h x)  h x'
      lemma' = ap 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 : U}  

 (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
  open import FunExt

  R : ℕ∞  ℕ∞  U
  R u v = Σ \x  u  f x  ×  v  g x

  r : (x : 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 (ap positivity c) (trans e (ap 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) = 
   (pr₁ lemma , pr₁(pr₂ lemma) , pr₂(pr₂ 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 = (R-positivity u v r) , (R-Pred u v r)

  lemma : (x : 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 : U}  

 (p : X  𝟙 + X)  Σ! \(h : X  ℕ∞)  diagram-commutes p h 

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

\end{code}

There is more formalization work to do (2017): By now we know that Σ!
(a form of unique existence) is better captured by the contractibility
of Σ type.