Coq 中的产品类型

Question

我在将参数传递给 coq 中的产品类型时遇到问题。我有一个看起来像这样的定义，

    Definition bar (a:Type) := a->Type.

我需要定义一个函数，该函数接收“a”和“bar a”制作的东西并输出它们的产品/订购对。所以我尝试了以下方法。

    Definition foo (a:Type)(b:bar a):= prod a b.

这给了我错误

术语“b”的类型为“bar a”，而预期的类型为“Type”。

这里真正令人困惑的是，

    Definition foo (a:Type) := prod a (bar a). 

工作得很好。显然“bar a”的类型为“Type”，所以我不确定如何修复我的原始定义。我怀疑我没有正确传递变量。

Answer 1

要查看错误，请在您的 foo 定义中展开 bar a：

Definition foo (a:Type)(b:a->Type):= prod a b.

现在应该清楚b 不是类型，它是从a 到Type 的函数。

由于您永远不会获得a 类型的对象，因此您无法将b 应用于任何事物，也无法从中获得Type。

对于第二个定义，再次展开以了解其工作原理：

Definition foo (a:Type) := prod a (a->Type).

a 和 a->Type 对于产品都是有效的 Type。