CantorPairingBoveCapretta.agda

open import Data.Nat using (ℕ ; zero ; suc)
open import Data.Product using (Σ ; _×_ ; _,_ ; ,_)
  renaming (proj₁ to fst ; proj₂ to snd ; curry to cu ; uncurry to uc)
open import Function using (id ; _∘_ ; _$_)
open import Level as L using (_⊔_)
open import Induction
open import Induction.Lexicographic
open import Induction.Nat
open import Relation.Binary.PropositionalEquality as ≡
  renaming (refl to <> ; sym to !_ ; cong₂ to ap₂) hiding ([_])

infixr 4 _⊚_

_⊚_ = ≡.trans

infixr 5 _$≡_

_$≡_ = ≡.cong

infix 4 _Π≡_

_Π≡_ : ∀ {l1}{X : Set l1}{l2}{Y : X → Set l2}(f g : (x : X) → Y x) → Set (l1 ⊔ l2)
f Π≡ g = ∀ x → f x ≡ g x

infix 1 _≅_

record _≅_ {lA }(A : Set lA){lB }(B : Set lB) : Set (lA ⊔ lB) where
  constructor mk
  field to       : A → B
        fr       : B → A
        fr∘to≈id : (fr ∘ to) Π≡ id
        to∘fr≈id : (to ∘ fr) Π≡ id

inj-suc : ∀ {m n : ℕ} → suc m ≡ suc n → m ≡ n
inj-suc <> = <>

module Pairing where

  data ⟨_⟩ : ℕ × ℕ → Set where
    zero :                           ⟨ zero  , zero  ⟩
    step : ∀ {a b} → ⟨ a , suc b ⟩ → ⟨ suc a ,     b ⟩
    jump : ∀ {a  } → ⟨ a , zero  ⟩ → ⟨ zero  , suc a ⟩

  length : ∀ {a b} → ⟨ a , b ⟩ → ℕ
  length (zero  ) = zero
  length (jump p) = suc (length p)
  length (step p) = suc (length p)

  _≡⟨_⟩ = λ n a,b → Σ ⟨ a,b ⟩ (_≡_ n ∘ length)
  _≡⟨⟩  = λ n → Σ _ λ a → Σ _ λ b → n ≡⟨ a , b ⟩

  ⟨,⟩-prop : ∀ {a b}(p q : ⟨ a , b ⟩) → p ≡ q
  ⟨,⟩-prop (zero  ) (zero  ) = <>
  ⟨,⟩-prop (step p) (step q) = step $≡ ⟨,⟩-prop p q
  ⟨,⟩-prop (jump p) (jump q) = jump $≡ ⟨,⟩-prop p q

  sameL : ∀ {n1 n2 a,b} → n1 ≡⟨ a,b ⟩ → n2 ≡⟨ a,b ⟩ → n1 ≡ n2
  sameL (p , <>) (q , <>) = length $≡ ⟨,⟩-prop p q

  sameR : ∀ {n a b c d} → n ≡⟨ a , b ⟩ → n ≡⟨ c , d ⟩ → a ≡ c × b ≡ d
  sameR (zero   , h1) (zero   , h2) = <> , <>
  sameR (zero   , <>) (step q , ())
  sameR (zero   , <>) (jump q , ())
  sameR (step p , <>) (zero   , ())
  sameR (step p , <>) (step q , h2) =
    let a , b = sameR (p , <>) (q , inj-suc h2) in suc $≡ a , inj-suc b
  sameR (step p , <>) (jump q , h2) with sameR (p , <>) (q , inj-suc h2)
  sameR (step p , <>) (jump q , h2)    | _ , ()
  sameR (jump p , <>) (zero   , ())
  sameR (jump p , <>) (step q , h2) with sameR (p , <>) (q , inj-suc h2)
  sameR (jump p , <>) (step q , h2)    | _ , ()
  sameR (jump p , <>) (jump q , h2) =
    let a , b = sameR (p , <>) (q , inj-suc h2) in <> , suc $≡ a

  incR : ∀ {a b} → ⟨ a , b ⟩ → ⟨ a , suc b ⟩
  incR (zero  ) = jump zero
  incR (jump p) = jump (step (incR p))
  incR (step p) = step (incR p)

  incL : ∀ {a b} → ⟨ a , b ⟩ → ⟨ suc a , b ⟩
  incL = step ∘ incR

  too : ∀ n → n ≡⟨⟩
  too zero = zero , zero , zero , <>
  too (suc n) with too n
  too (suc n) | a , zero  , p , q = zero  , suc a , jump p , suc $≡ q
  too (suc n) | a , suc b , p , q = suc a ,     b , step p , suc $≡ q

  to : ℕ → ℕ × ℕ
  to n = let a , b , _ = too n in a , b

  domFrom : ∀ a,b → ⟨ a,b ⟩
  domFrom = build [ rec-builder ⊗ rec-builder ] ⟨_⟩ (uc me) where
    me : ∀ a b → Rec L.zero (cu ⟨_⟩ a) b × Rec L.zero (λ x → (b : ℕ) → ⟨ x , b ⟩) a → ⟨ a , b ⟩
    me (zero )(zero )(p , q) = zero
    me (zero )(suc b)(p , q) = incR p
    me (suc a)(    b)(p , q) = step (q (suc b))

  from : ℕ × ℕ → ℕ
  from = length ∘ domFrom

  iso₁ : from ∘ to Π≡ id
  iso₁ n = let a , b , p , q = too n ; d = domFrom (a , b) in
           sameL (d , <>) (p , <>) ⊚ ! q

  iso₂ : to ∘ from Π≡ id
  iso₂ a,b = let d = domFrom a,b ; _ , _ , p , q = too (length d) in 
             uc (ap₂ _,_) $ sameR (p , q) (d , <>)

pairing : ℕ ≅ ℕ × ℕ
pairing = mk to from iso₁ iso₂ where open Pairing