依赖类型是依赖于类型术语的类型。所以我想知道依赖类型是否可以由其自己的类型的术语进行索引？我尝试的是这个
Parameter Obj: Type.
Parameter a: Obj.
Parameter foo: Obj -> Type.
Parameter b : foo a.
Parameter boo : Obj -> Type.
Fail Parameter c : boo b.
自 The term "b" has type "foo a" while it is expected to have type "Obj". 以来失败。我试图用依赖类型理论做什么吗？我如何使用 Coq 实现它？
这在我所知道的任何系统中都是不可能的。它在阿格达间接工作，但在Coq中没有任何工作。在 Agda 中，您需要使用不同的类型包装索引：
-- forward declaration
data A : Set
data B : A -> Set
data A where
wrap : B -> A
data B where
-- list your other constructors here
Coq尚不支持这种形式的索引(称为"感应-感应"(。