Martin Escardo, Chuangjie Xu, 2012.

As a simple application of coinduction and corecursion, 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.


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

module CoNaturalsExercise where

open import Cantor
open import Two
open import GenericConvergentSequence
open import SetsAndFunctions
open import Naturals hiding (_+_)
open import CoNaturals
open import Equality
open import CurryHoward
open import Extensionality
open import Sequence

incl-is-a-section :  \(retr : ₂ℕ  ℕ∞)  retr  incl  id
incl-is-a-section  = ∃-intro retr (funext lemma)
  f-retr :   ₂ℕ  𝟙 + ₂ℕ
  f-retr  α = in₀ *
  f-retr  α = in₁ α 

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

  retr : ₂ℕ  ℕ∞
  retr = ℕ∞-corec p-retr

  retr-spec : P  retr  (𝟙+ retr)  p-retr
  retr-spec = ∃-elim(homomorphism-existence p-retr)

  retr-spec₀ : ∀(α : ₂ℕ)  hd α    retr α  Zero
  retr-spec₀ α r = alg-morphism-Zero p-retr retr retr-spec α * lemma
    lemma : p-retr α  in₀ *
    lemma = cong  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
    lemma : p-retr α  in₁(tl α)
    lemma = cong  b  f-retr b (tl α)) r

  R : ℕ∞  ℕ∞  Prp
  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₁ 
    lemma₀ : positivity w    positivity u  positivity v
    lemma₀ r = cong positivity claim₃
      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₄)
      claim₀ : positivity(retr(incl w))   
      claim₀ = cong positivity (retr-spec₁(incl w) r)
      claim₁ : positivity(retr(incl w))  positivity u 
      claim₁ = cong positivity c
      claim₂ : positivity u  
      claim₂ = trans (sym claim₁) claim₀
      claim₃ : positivity w  positivity v
      claim₃ = cong 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₁)
    lemma₀ : retr(incl(Pred w))  Pred u
    lemma₀ = trans claim claim₀
     claim₀ : Pred(retr(incl w))  Pred u
     claim₀ = cong Pred c
     claim :  retr(incl(Pred w))  Pred(retr(incl w))
     claim = two-equality-cases claim₁ claim₂
       claim₁ : isZero w  retr(incl(Pred w))  Pred(retr(incl w))
       claim₁ r = Lemma[x≡z→y≡z→x≡y] c₃ c₅
         c₀ : w  Zero
         c₀ = isZero-equal-Zero r
         c₁ : Pred w  Zero
         c₁ = cong Pred c₀
         c₂ : incl (Pred w) 0  
         c₂ = cong (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₅ = cong Pred c₄
       claim₂ : positive w  retr(incl(Pred w))  Pred(retr(incl w))
       claim₂ r = Lemma[x≡z→y≡z→x≡y] c₃ c₁
         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 (cong Pred c₀) Pred-Succ-u-is-u
         c₃ : retr(incl(Pred w))  retr(tl(incl w))
         c₃ = refl

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

  R-bisimulation : ℕ∞-bisimulation R
  R-bisimulation u v r = ∧-intro (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)