E[G] |- T : s sÎ S x Ï G È E |
WF(E)[G::(x:T)] |
|
|
WF(E)[G] i<j |
E[G] |- Type(i) : Type(j) |
WF(E)[G] (x:T)ÎG |
E[G] |- x : T |
WF(E)[G] (c:T) Î E |
E[G] |- c : T |
E[G] |- T : s1 E[G::(x:T)] |- U : s2 s1Î{Prop, Set} or s2Î{Prop, Set} |
E[G] |- (x:T)U : s2 |
E[G] |- T : Type(i) E[G::(x:T)] |- U : Type(j) i£ k j £ k |
E[G] |- (x:T)U : Type(k) |
E[G] |- (x:T)U : s E[G::(x:T)] |- t : U |
E[G] |- [x:T]t : (x:T)U |
E[G] |- t : (x:U)T E[G] |- u : U |
E[G] |- (t u) : T{x/u} |