The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

This works because sigT is "template universe polymorphic" 
https://coq.github.io/doc/master/refman/language/cic.html#template-polymorphism 
which makes every application inhabit as low a universe as the arguments 
allow.

There's also "universe polymorphism" 
https://coq.github.io/doc/master/refman/addendum/universe-polymorphism.html 
which is more regular (eg can be used for any definition rather than 
just inductives) but currently cannot be instantiated with Prop.

Gaëtan Gilbert

On 23/09/2019 05:05, Jeremy Dawson wrote:
> Hi,
>
> I have an example where I'm confused about the rules regarding types.
>
> I have a function GiT of the following type
>
> ljt_dec < Check GiT.
> GiT : list PropF -> PropF -> nat -> Prop
>
> ljt_dec < Check (GiT Γ P 0).
> GiT Γ P 0 : Prop
>
> The following is accepted without a type error
>
> ljt_dec < Check (existsT2 d : nat, GiT Γ P d).
> existsT2 d : nat, GiT Γ P d : Set
>
> existsT2 is notation for sigT ...
>
> ljt_dec < Check (sigT (fun d : nat => GiT Γ P d)).
> existsT2 d : nat, GiT Γ P d : Set
>
> ljt_dec < Check sigT.
> sigT : forall A : Type, (A -> Type) -> Type
>
> but sigT wants a body of type Type (ie nat -> Type)
> but in the example works with a body of type
> (nat -> Prop)
>
> and sigT should return result type of Type, but here
> returns a result of type Type
>
> Sometimes (often) coq objects when you get Prop, Set and
> Type mixed up, and use the wrong one, here not at all.
>
> I'd like to understand why this is so
>
> Thanks
>
> Jeremy