Система F Церковные цифры в Агде

Question

Я хотел бы протестировать некоторые определения в системе F, используя Agda в качестве моего средства проверки типов и оценщика.

Моя первая попытка ввести натуральные числа в Церкви была написана

Num = forall {x} -> (x -> x) -> (x -> x)

Который будет использоваться как псевдоним обычного типа:

zero : Num
zero f x = x

Однако определение Num не проверяет тип (вид?). Каков наиболее подходящий способ заставить его работать и быть как можно ближе к системной нотации F?

Answer 1

Следующая проверка типа

Num : Set₁
Num = forall {x : Set} -> (x -> x) -> (x -> x)

zero : Num
zero f x = x

но, как вы видите Num : Set₁, это может стать проблемой, и вам понадобится --type-in-type