[Agda] Defining large numbers without recursion, with short programs

[effectfully]

Neat trick. BTW, you can avoid these giant implicit arguments by
wrapping the N into a record (my emacs doesn't want to display 𝟘 𝟙
𝟚 𝟛 properly):

{-# OPTIONS --no-pattern-matching #-}

U = Set

data ℕ : U where
 zero : ℕ
 succ : ℕ → ℕ

record N X : U where
  constructor #
  field el : (X → X) → (X → X)
open N

b0 b1 b2 b3 : {X : U} → N X
b0 = # λ s z → z
b1 = # λ s z → s z
b2 = # λ s z → s(s z)
b3 = # λ s z → s(s(s z))

suc : {X : U} → N X → N X
suc n = # λ s z → s (el n s z)

add : {X : U} → N X → N X → N X
add m n = # λ s z → el m s (el n s z)

N-rec : {X : U} → (X → X) → X → (N X → X)
N-rec s z m = el m s z


mul : {X : U} → N X → N(N X) → N X
mul m = N-rec (add m) b0

exp : {X : U} → N(N X) → N(N X) → N X
exp n = N-rec (λ m → mul m n) b1

decode : N ℕ → ℕ
decode = N-rec succ zero

large : ℕ
large = decode
 (exp b2
 (exp b2
 (exp b2
 (exp b2
 (exp b2
 (exp b2
 (exp b2
 (exp b2
 (exp {?} b2
      b2)))))))))

Then Agda infers

    N (N (N (N (N (N (N (N ℕ)))))))

in the hole above.