System F Church numerals in Agda

Question

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?

Answer 1

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