The Coq mailing list

[Jean-Francois Dufourd <dufourd AT dpt-info.u-strasbg.fr>]

Hi,

I'm trying to (impredicatively) define the type Nat in Coq
(without the option - impredicative-set, which works well).

I write:

Definition Nat:=forall X:Type,(X->X)->X-> X.

Definition succ(n:Nat):Nat:=
fun(X:Type)(f:X->X)(z:X) => (f (n X f z)).

Definition add(n m:Nat):Nat:=
fun(X:Type)(f:X->X)(z:X) => m X f (n X f z).

Definition mult(n m:Nat):Nat:=
fun(X:Type)(f:X->X)(z:X) => m X (n X f) z.

All that is OK. But, when I write an other version of mult:

Definition mult1(n m:Nat):Nat:=
n Nat (add m) zero.

Coq answers "Universe inconsistency".

I interprete this mistake as the violation of the typing rules, because
Nat is probably of higher Type level as the X of its definition.

Is this true ? Does a means exist for circumventing this problem ?

Thank you !

Jean-Franc,ois Dufourd