The Coq mailing list

[Francois Puitg <puitg AT imag.fr>]

Hello,

Two questions about the CiC, chapter 4 of the Coq reference manual.

1) Section 4.1.1 p.  82 tells us that Prop, Set : Type(0), whereas the
Ax rules of section 4.2 state that Prop : Type(p) and Set : Type(q).

2) I can't see how typecheck nat  -> Prop with the  Prod rules p.  85.
Let's simplify them giving up contexts and the global environment, and
switching to non dependent product. We get :


T : s           s belongs to S          U : Prop
------------------------------------------------
                T -> U : Prop


T : s           s belongs to {Prop, Set}                U : Set
---------------------------------------------------------------
                        T -> U : Set


T : Type(i)             U : Type(j)
-----------------------------------     with i, j <= k
          T -> U : Type(k)


We  have T = nat and  U = Prop.  First rule  can't  apply since Prop :
Type, and not Prop.  Second rule neither because Prop  : Type  and not
Set. Third rule fails since nat : Set and not Type(i).