I would like to test some definitions in system F using Agda as my typechecker and evaluator.
My first attempt to introduce Church natural numbers was by writing
Num = forall {x} -> (x -> x) -> (x -> x)
Which would be used just like a regular type alias:
zero : Num
zero f x = x
However the definition of Num does not type(kind?)check. What is the most proper way to make it working and be as close as possible to the system F notation?
The following would typecheck
Num : Set₁
Num = forall {x : Set} -> (x -> x) -> (x -> x)
zero : Num
zero f x = x
but as you see Num : Set₁, this might become a problem and you'll need --type-in-type