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.

\begin{code}

module CoNaturalsExercise where

open import Cantor
open import Two
open import GenericConvergentSequence
open import SetsAndFunctions
open import Naturals
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 (extensionality lemma)
where
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
where
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
where
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₁
where
lemma₀ : positivity w ≡ ₀ → positivity u ≡ positivity v
lemma₀ r = cong 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₀ = 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₁)
where
lemma₀ : retr(incl(Pred w)) ≡ Pred u
lemma₀ = trans claim claim₀
where
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₂
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₁ = 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₁
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 (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)

\end{code}