The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Sat, 03 May 2014 10:44:12 +0100,
Matej Kosik 
<5764c029b688c1c0d24a2e97cd764f AT gmail.com>
 a écrit :

> Dear all,
> 
> While I was trying to grok the Coq inference rules (as stated in the
> Coq'Art book), I came across this: (pages 91,92)
> 
>         E,Γ ⊢ A : Type(i)    E,Γ ∷ (a:A) ⊢ B : Type(j)    i ≤ k    j
> ≤ k Prod
> ──────────────────────────────────────────────────────────────── E,Γ
> ⊢ ∀ a:A,B : Type(k)
> 
> Here I started to wonder, what are the reasons for the stated
> constraints:
> 
>     i ≤ k
>     j ≤ k
> 
> Why (any) weaker condition, such as
> 
>     k ≤ i
>     k ≤ j
> 
> , could cause problems?
> 
> I either failed to deduce it from what I know (possible),
> or there is something important I do not know (likely) :-)
> 
> Thanks in advance for any help.

I guess it is related to Girard paradox.