Formality-Agda-Nat.agda

{-# OPTIONS --type-in-type         #-}
{-# OPTIONS --no-positivity-check  #-}
{-# OPTIONS --no-termination-check #-}

-- Agda obviously doesn't have self-types, so we fake them here.
postulate
  ι : {A : Set} -> (A -> Set) -> Set
  gen : {A : Set} {B : A -> Set} -> ∀ x -> B x -> ι B
  inst : {A : Set} {B : A -> Set} -> ∀ x -> ι B -> B x

NatBody : Set

-- The type of lambda-encoded natural numbers. Just a wrapper around `NatBody` that allows to
-- break the cycle.
record Nat : Set where
  inductive
  constructor ToNat
  field fromNat : NatBody
open Nat

zero : Nat
suc : Nat -> Nat

-- The body of the type of lambda-encoded natural numbers.
NatBody = ι λ n -> (P : Nat -> Set) -> (∀ {m} -> P m -> P (suc m)) -> P zero -> P n

-- The eliminator. Note that `inst` must always be instantiated with the thing being eliminated,
-- because this is how it behaves in System S.
elimNat : (P : Nat -> Set) -> (∀ {m} -> P m -> P (suc m)) -> P zero -> ∀ n -> P n
elimNat P s z n = inst n (fromNat n) P s z

-- The constructors. Note that `gen` must always be instantiated with the thing being defined,
-- because this is how it behaves in System S.
zero = ToNat (gen zero λ _ s z -> z)
suc n = ToNat (gen (suc n) λ P s z -> s (elimNat P s z n))