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}

{-# 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)
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}