Martin Escardo, Chuangjie Xu, 2012.

As a simple application of coinduction and corecursion on ℕ∞, one can
show that the the inclusion map incl : ℕ∞ → ₂ℕ is part of a
retraction.

This exercise is artificial: a direct construction and proof of the
retraction would be shorter and perhaps clearer. However, it does
illustrate how co-recursion and co-induction can be used.

Recall that a retraction is a pair of maps r : X → Y and s : Y → X
such that r ∘ s : Y → Y is the identity, where r is called the
retraction and s the section. In this case, it follows that 
s ∘ r : X → X is idempotent, and s is an injection and r is a
surjection. When such maps exists one says that Y is a retract of X.

The idea of the construction of the retraction is that we "read"
digits from α until we find a zero or forever, and count how long
this took.

\begin{code}

{-# OPTIONS --without-K --exact-split --safe #-}

module CoNaturalsExercise where

open import SpartanMLTT
open import Naturals
open import Two
open import CoNaturals
open import GenericConvergentSequence
open import Sequence

incl-is-a-section : Σ \(retr : (  𝟚)  ℕ∞)  retr  incl  id
incl-is-a-section  = retr , (funext lemma)
 where
  open import FunExt
  
  f-retr : 𝟚  (  𝟚)  𝟙 + (  𝟚)
  f-retr  α = inl *
  f-retr  α = inr α 

  p-retr : (  𝟚)  𝟙 + (  𝟚)
  p-retr α = f-retr(hd α)(tl α)

  retr : (  𝟚)  ℕ∞
  retr = ℕ∞-corec p-retr

  retr-spec : P  retr  (𝟙+ retr)  p-retr
  retr-spec = pr₂(homomorphism-existence p-retr)

  retr-spec₀ : (α :   𝟚)  hd α    retr α  Zero
  retr-spec₀ α r = alg-morphism-Zero p-retr retr retr-spec α * lemma
   where 
    lemma : p-retr α  inl *
    lemma = ap  b  f-retr b (tl α)) r

  retr-spec₁ : (α :   𝟚)  hd α    retr α  Succ(retr(tl α))
  retr-spec₁ α r = alg-morphism-Succ p-retr retr retr-spec α (tl α) lemma
   where 
    lemma : p-retr α  inr(tl α)
    lemma = ap  b  f-retr b (tl α)) r

  R : ℕ∞  ℕ∞  U
  R u v = Σ \w  retr(incl w)  u × w  v 

  r : (u : ℕ∞)  R (retr(incl u)) u
  r u = (u , refl , refl)

  R-positivity : (u v : ℕ∞)  R u v  positivity u  positivity v
  R-positivity u v (w , c , d) = 
   two-equality-cases lemma₀ lemma₁ 
   where 
    lemma₀ : positivity w    positivity u  positivity v
    lemma₀ r = ap positivity claim₃
     where 
      claim₀ : retr(incl w)  Zero
      claim₀ = retr-spec₀(incl w) r
      claim₁ : v  Zero
      claim₁ = trans (sym d) (isZero-equal-Zero r)
      claim₂ : retr(incl w)  v
      claim₂ = trans claim₀ (sym claim₁)
      claim₃ : u  v
      claim₃ = trans (sym c) claim₂

    lemma₁ : positivity w    positivity u  positivity v
    lemma₁ r = trans claim₂ (sym claim₄)
     where 
      claim₀ : positivity(retr(incl w))   
      claim₀ = ap positivity (retr-spec₁(incl w) r)
      claim₁ : positivity(retr(incl w))  positivity u 
      claim₁ = ap positivity c
      claim₂ : positivity u  
      claim₂ = trans (sym claim₁) claim₀
      claim₃ : positivity w  positivity v
      claim₃ = ap positivity d
      claim₄ : positivity v  
      claim₄ = trans (sym claim₃) r

  R-Pred : (u v : ℕ∞)  R u v  R(Pred u)(Pred v)
  R-Pred u v (w , c , d) = (Pred w , lemma₀ , lemma₁)
   where
    lemma₀ : retr(incl(Pred w))  Pred u
    lemma₀ = trans claim claim₀
     where
     claim₀ : Pred(retr(incl w))  Pred u
     claim₀ = ap Pred c
     claim :  retr(incl(Pred w))  Pred(retr(incl w))
     claim = two-equality-cases claim₁ claim₂
      where 
       claim₁ : isZero w  retr(incl(Pred w))  Pred(retr(incl w))
       claim₁ r = Lemma[x≡z→y≡z→x≡y] c₃ c₅
        where
         c₀ : w  Zero
         c₀ = isZero-equal-Zero r
         c₁ : Pred w  Zero
         c₁ = ap Pred c₀
         c₂ : incl (Pred w) 0  
         c₂ = ap (hd  incl) c₁
         c₃ : retr(incl (Pred w))  Zero
         c₃ = retr-spec₀(incl (Pred w)) c₂
         c₄ : retr(incl w)  Zero
         c₄ = retr-spec₀(incl w) r
         c₅ : Pred(retr(incl w))  Zero
         c₅ = ap Pred c₄
       claim₂ : positive w  retr(incl(Pred w))  Pred(retr(incl w))
       claim₂ r = Lemma[x≡z→y≡z→x≡y] c₃ c₁
        where
         c₀ : retr(incl w)  Succ(retr(tl(incl w)))
         c₀ = retr-spec₁ (incl w) r
         c₁ : Pred(retr(incl w))  retr(tl(incl w))
         c₁ = trans (ap Pred c₀) Pred-Succ-u-is-u
         c₃ : retr(incl(Pred w))  retr(tl(incl w))
         c₃ = refl

    lemma₁ : Pred w  Pred v
    lemma₁ = ap Pred d

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

  lemma : (u : ℕ∞)  retr(incl u)  u
  lemma u = ℕ∞-coinduction R R-bisimulation (retr(incl u)) u (r u)

\end{code}