The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Helmut,

 

maybe it helps you to enable “Display all low level contents” in CoqIDE.

 

For Check sig you then get:

 

sig

     : forall A : Type@{Coq.Init.Specif.1}, (A -> Prop) -> Type@{Coq.Init.Specif.1}

 

Essentially sig is polymorphic over universe levels (the logicians may forgive me if this is not the right wording). Type@{Coq.Init.Specif.1} can be a Type of any universe level, including Set. As soon as A is known to be nat, Type@{Coq.Init.Specif.1} is bound to be Set, which then determines the result type. If sig would not be universe polymorphic, one would need separate definitions for Set, and all the levels of Type.

 

Typically Coq handles the universe restrictions automatically, so the Universe parameters (the @{…}) are not shown.

 

I guess you already read something like https://en.wikipedia.org/wiki/Impredicativity and understand the basic concept why this is needed.

 

Best regards,

 

Michael

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928