第一类错误
第一个类型错误的问题
constant C : �� (b : B), Type</code>
是你不能说的
b : B
因为
B
是一个
功能
（没有定义）类型
A -> Type
，即
B
是一个
值
，不是一种类型。
提出索赔是没有意义的
b : 1
要么
b : “xyz”
要么
b : (�� a : A, Type)
。
例如。以下是可行的，因为
B a : Type
：
constant C : �� (b : B a), Type</code>
第二类错误
第二种类型的错误
constant C’ : �� (B : A), (�� (b : B), Type)</code>
源于不知道的事实
B
是一种类型，我们都知道
B
是类型的某种价值（居民）
A
。能够使用
B
这样，你需要这样的东西：
constant C’ : �� (B : Type), (�� (b : B), Type)</code>
我们明确地说
B
是一种类型。
第三类错误
constant C’’ : B -> Type</code>
未能进行类型检查的原因与第一种情况相同。
B
是一个函数值，虽然我们需要一个类型 - 这就是原因
constant B : A -> Type
作品。