The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

Dear Jeremy,

I think your question is related to cumulativity
ie Prop and Set are both included in Type_0
and Type_i is included in Type_{i+1}

There are other instances of the use of the
cumulativity rule like:

Check nat_rect.

nat_rect : forall P : nat -> Type, P 0 -> (forall n, P n -> P (S n)) -> 
forall n, P n

Definition nat_ind (P : nat -> Prop) := nat_rect P.

Best,

Dominique


----- Mail original -----
> De: "Jeremy Dawson" 
> <Jeremy.Dawson AT anu.edu.au>
> À: "coq-club" 
> <coq-club AT inria.fr>
> Envoyé: Lundi 23 Septembre 2019 05:05:13
> Objet: [Coq-Club] sigT and Prop

> 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