Finding predecessor (or, destructors?) of Church Numerals using the relation outT = (| F inT |)

numeral.agda

module numeral where

infixl 40 _∘_
infixr 60 1+ⁿ_

-- small prelude
_∘_ : {A B C : Set} → (B → C) → (A → B) → A → C
f ∘ g = λ x → f (g x)

data ℕ : Set where
  0ⁿ : ℕ
  1+ⁿ_ : ℕ → ℕ

{-
   Fᵗ : Functor
      Fᵗ X = 1 + X
   or Fᵗ X = Z | S X
-}
Fᵗ : Set → Set → Set
Fᵗ α X = α → (X → α) → α

Z : (X α : Set) → Fᵗ α X
Z _ _ = λ left right → left

S : (X α : Set) → X → Fᵗ α X
S _ _ x = λ left right → right x

Fᶠ : (A B : Set) → (A → B) → (α : Set) → Fᵗ α A → Fᵗ α B
Fᶠ _ _ f _ FᵗA = λ left right → FᵗA left (right ∘ f)

-- the fixed point of Fᵗ, kind of... μFᵗ ?
T : Set → Set
T β = Fᵗ β β

FᵗT : Set → Set
FᵗT α = Fᵗ α (T α)

inᵀ : (α : Set) → Fᵗ α (T α) → T α
inᵀ _ FᵗT = λ z f → FᵗT z (λ n → f (n z f))

-- now the fold
foldᵀ : (A : Set) → (Fᵗ A A → A) → ((α : Set) → T α) → A
foldᵀ A FᵗA n = FᵗA (λ z f → n A z f)

h : (α β : Set) → Fᵗ β (FᵗT α) → Fᵗ β (T α)
h α = Fᶠ (FᵗT α) (T α) (inᵀ α)

{-
haa : (α : Set) → Fᵗ (FᵗT α) (FᵗT α) → Fᵗ (FᵗT α) (T α)
haa α = h α (FᵗT α)

hb : (α : Set) → Fᵗ (FᵗT α) (FᵗT α) → FᵗT α
hb α F = haa α F (Z (T α) α) (S (T α) α)
-}

outᵀ : (α : Set) → ((β : Set) → T β) → Fᵗ α (T α)
outᵀ α = foldᵀ (FᵗT α) (λ F → h α (FᵗT α) F (Z (T α) α) (S (T α) α))

-- numbers
zero : (α : Set) → T α
zero α = inᵀ α (Z (T α) α)

suc : (α : Set) → T α → T α
suc α = λ n → inᵀ α (S (T α) α n)

three : (α : Set) → T α
three α = suc α (suc α (suc α (zero α)))

two : (α : Set) → T α
two α = outᵀ (T α) three (zero α) (λ n → n (zero α) (suc α))

-- from church numerals to ℕ
FN→N : Fᵗ ℕ ℕ → ℕ
FN→N FᵗN = FᵗN 0ⁿ 1+ⁿ_

church2nat : ((α : Set) → T α) → ℕ
church2nat = foldᵀ ℕ FN→N

data _≡_ {A : Set} (a : A) : A → Set where
  refl : a ≡ a

twoistwo : church2nat two ≡ (1+ⁿ 1+ⁿ 0ⁿ)
twoistwo = refl

threeisthree : church2nat three ≡ (1+ⁿ 1+ⁿ 1+ⁿ 0ⁿ)
threeisthree = refl

{-

outᵀ : T → F T

   outᵀ = foldᵀ h

⇔ { universal property of foldᵀ }

   foldᵀ h ∘ inᵀ = h ∘ Fᶠ (foldᵀ h)

⇔  { outᵀ ∘ inᵀ = id }

   id = h ∘ Fᶠ (foldᵀ h)

⇒  { Leibniz???? is it ⇒ or ⇐ ? }

   id ∘ Fᶠ inᵀ = h ∘ Fᶠ (foldᵀ h) ∘ Fᶠ inᵀ

⇔  { F functor }

   Fᶠ inᵀ = h ∘ Fᶠ ( foldᵀ h ∘ inᵀ )

⇔  { F functor, foldᵀ h ∘ inᵀ = id }

   Fᶠ inᵀ = h

-}