3(church)

%default total

record Church where
  constructor MkNat
  natF : {a : Type} -> (a -> a) -> a -> a

zero : Church
zero = MkNat $ \_, x => x

succ : Church -> Church
succ n = MkNat $ \f, x => f ((natF n f) x)

one : Church
one = succ zero

churchToNat : Church -> Nat
churchToNat n = (natF n S) Z

plus : Church -> Church -> Church
plus n m = natF m succ n

mult : Church -> Church -> Church
mult n m = natF m (plus n) zero

Product : (a : Type) -> (b : Type) -> Type
Product a b = (ty : Type) -> (a -> b -> ty) -> ty

pair : a -> b -> Product a b
pair l r = \_, f => f l r

first : Product a b -> a
first p = p _ (\x, _ => x)

second : Product a b -> b
second p = p _ (\_, x => x)

zeroP : Product Church Church
zeroP = pair zero zero

succP : Product Church Church -> Product Church Church
succP p = pair (succ $ first p) (first p)

nWithPred : Church -> Product Church Church
nWithPred n = (natF n succP) zeroP

pred : Church -> Church
pred = second . nWithPred

minus : Church -> Church -> Church
minus n m = natF m pred n

main : IO()
main = putStrLn . show . churchToNat $ (minus (plus one one) one)