dependent-type - 如何在精益中使用 Pi 类型编写非依赖产品的定义？

Question

我正在阅读第 7 章——“精益中的定理证明”的归纳类型。

我想知道如何以更扩展或“原始”的形式编写依赖非依赖产品的定义。

1. 看起来教程中给出的定义会自动推断出一些细节： inductive prod1 (α : Type u) (β : Type v) | mk : α → β → prod1

2. 一些实验允许填写细节 inductive prod2 (α : Type u) (β : Type v) : Type (max u v) | mk : α → β → prod2

3. 但是以完全扩展的形式给出定义，使用 Pi 类型无法进行类型检查： inductive prod3 : Π (α : Type u) (β : Type v), Type (max u v) | mk : α → β → prod3

正确的书写方式是prod3什么？

最后，下面的定义是否等同于prod1and prod2，即类型检查器是否总能推断出αand的正确类型全域β？

4. inductive prod4 (α : Type) (β : Type) | mk : α → β → prod4

Answer 1

首先，请注意，您的类型没有任何依赖关系。从属产品只是 Pi 类型本身的另一个名称（Pi 源自索引产品的常用数学符号）。

您的prod2类型是正确的最大显式版本prod1。在prod3中，您将 α 和 β 从归纳参数更改为indices，正如您所注意到的，由于与宇宙相关的原因，这不起作用。通常，索引用于定义归纳类型族，如第 7.7 节中所述。

最后，Type您使用的 atomicprod4是Type 1. 您可以使用Type*自动推断 Universe 参数。