⑧.2带依赖类型的演算 定类规则 b:K(对基调中的每个类型常量b:K) (cst这∈TTK T t:K Tσ：Tpe T,x:o:Type (vark) T Πx:O2):Tpe (Type IntroΠ O:Πx:OK)T M:O M:[Mix]K (k Elim） T K1-K 0:K2 (kind eq)8.2 带依赖类型的演算 • 定类规则  b :  (对基调中的每个类型常量b :  ) (cstk ) (vark ) (Type Intro ) (k Elim) (kind eq)  1 : Type , x : 1 2 : Type  ( x : 1 . 2 ) : Type t :       t :   1 : (x:2 .)  M : 2  1M : [M/x]   : 1  1=2   : 2