如何在精益中使用Pi類型編寫非相關產品的定義？

Question

我正在努力通過「定理證明在精益中」的chapter 7 – Inductive Types。

我想知道如何編寫依賴非獨立產品的定義在更多擴展或「原始」形式。

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的正確方法？

最後，是以下定義相當於prod1和prod2，即可以類型檢查器總是推斷α和β正確類型宇宙？

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

Answer 1

首先，請注意，沒有任何依賴你的類型。 相關產品只是Pi類型本身的另一個名稱（來自通常的索引產品數學表示法的Pi）。

您的prod2類型是prod1的正確最大顯式版本。在prod3中，您將α和β從感應參數更改爲索引，正如您注意到的，因爲與Universe相關的原因而無法解決。一般來說，指數用於定義7.7中的歸納類型族。

最後，您在prod4中使用的原子Type是Type 1的縮寫。您可以使用Type*來自動推斷Universe參數。