module Church where
open import Agda.Primitive

Church : {l : Level} -> Set l -> Set l
Church A = (A -> A) -> (A -> A)

Nat = {A : Set} -> Church A
Nat₁ = {A : Set₁} -> Church A
Nat₂ = {A : Set₂} -> Church A

c0 : Nat
c0 = s z -> z

c1 : Nat
c1 = s z -> s z

c2 : Nat
c2 = s z -> s (s z)

add : Nat -> Nat -> Nat
add a b s z = b s (a s z)

mul : Nat -> Nat -> Nat
mul a b s z = b (a s) z

-- First signs of the type growing:
-- exp : {A : Set} -> Church A -> Church (A -> A) -> Church A
exp : Nat -> Nat -> Nat
exp a b = b a

tetr : Nat -> Nat₁ -> Nat
tetr k n = n (exp k) c1

pent : Nat -> Nat₁ -> Nat
pent k n = n (tetr k) c1 -- error