The following encoding of Nats is used in some Cedille sources:
cNat : ★
cNat = ∀ X : ★ . X ➔ (∀ R : ★ . (R ➔ X) ➔ R ➔ X) ➔ X
cZ : cNat
cZ = Λ X . λ z . λ s . z
cS : ∀ A : ★ . (A ➔ cNat) ➔ A ➔ cNat
cS = Λ A . λ e . λ d . Λ X . λ z . λ s . s · A (λ a . e a · X z s) d
I wonder if this is a common encoding used in other languages (Agda, Idris, Coq). If so, how can I interpret it, how it works, and how can I construct members of this type?
I've tried applying cS as in:
c0 = cZ
c1 = (cS -CNat (λ p : CNat . p) C0)
c2 = (cS -CNat (λ p : CNat . p) C1)
c3 = (cS -CNat (λ p : CNat . p) C2)
Which checks, but looks rather weird to me. p could be replaced by any cNat inside lambdas, for example. This doesn't look isomorphic to cNat to me. I guess I don't get this structure.
Edit by JC (too long for a comment, isn't an answer at all). For those who want to experiment, here's an Agda rendering.
module Mendler where
open import Level renaming (suc to lsuc)
open import Data.Nat
cNat : (ℓ : Level) → Set (lsuc ℓ)
cNat ℓ = (X : Set ℓ) → X → ((R : Set ℓ) → (R → X) → R → X) → X
private
variable
ℓ : Level
cZ : cNat ℓ
cZ X z s = z
cS : (A : Set ℓ) → (A → cNat ℓ) → A → cNat ℓ
cS A e d X z s = s A (λ a → e a X z s) d
c0 : cNat 0ℓ
c0 = cZ
c1 : cNat 0ℓ
c1 = cS ℕ (λ _ → c0) 0
