The Coq mailing list

[Eddy Westbrook <westbrook AT kestrel.edu>]

Requiring k to be greater than or equal to both i and j is just another way 
to say that k must be at least the maximum of i and j. The idea here is that 
(unless B is a Prop, where you can use impredicativity) in order to form a 
type forall (a:A), B, you need to go to a universe that is at least big 
enough (high enough i) to contain both A and B. If k were less than the 
universe level i for A, then k wouldn’t be big enough to even get A, let 
alone to get forall (a:A), B.

Hope that helps,
-Eddy

On May 3, 2014, at 2:44 AM, Matej Kosik 
<5764c029b688c1c0d24a2e97cd764f AT gmail.com>
 wrote:

> 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.