8.2 带依赖类型的演算 集合族 {Bx)x∈A的每个集合Bx)对应一个以类型A的 元素x为索引的类型 -这一族类型构成一个以类型A的元素为索引的类 型族8.2 带依赖类型的演算 • 集合族 – {B(x) | xA}的每个集合B(x)对应一个以类型A的 元素x为索引的类型 – 这一族类型构成一个以类型A的元素为索引的类 型族