8.2带依赖类型的演算 定型规则 C:σ (对基调中的每个项常量c:o x:o∈TT o:Type T x:O T 1:Type T,x:o1 M:02 ΠIntro T 入x:O1M:Πx:OO2) TM1:Πx:o.O)T M2:O1 ΠElim) MM,:[Mx]o M:1Tσ=2 (type eq) M:O28.2 带依赖类型的演算 • 定型规则  c :  (对基调中的每个项常量c : ) (cst) (var) ( Intro) ( Elim) (type eq) x :      : Type  x :   1 : Type , x : 1 M :2  x: 1 .M : ( x : 1 . 2 )  M1 : (x:1 .2 )  M2 : 1  M1M2 : [M2 /x]2  M : 1  1=2  M : 2