Agda中的类型层次结构

Question

我试图弄清楚Agda中类型层次结构的工作原理。

假设我定义了一个集合类型X：

X : Set 

然后开始构造归纳类型。

data Y : X -> Set where

X -> Set 的类型是什么？它是 Set 还是 Type？

谢谢！

- AnaK

Answer 1

那为什么不直接问Agda本身呢？我将使用优秀的Emacs Agda模式。我们从以下内容开始：

module Hierarchy where

postulate
  X : Set

data Y : X → Set where
  -- empty

我们需要使用C-c C-l来加载文件；这会对文件进行类型检查，将?转换为占位符（hole）, 进行语法高亮等操作。

现在，有一个通过C-c C-d可用的“推断(推导)类型”命令，让我们使用它：

> C-c C-d
Expression:
> Y
X → Set

好的，这很有道理。我们定义了Y：X→Set，所以这不应该让人感到意外。让我们再问一次：

> C-c C-d
Expression:
> X → Set
Set₁

所以，你现在知道了：Y : X → Set : Set₁。

---

尽管第一部分回答了问题并向您展示了如何自行检查此内容，但每次这样做都会变得乏味，至少是这样。以下是它的工作原理：

为避免悖论，我们要求：

Set i : Set (i + 1)

这将为你提供（无限）层级的Set集合。如果您拥有Set:Set（这是通过Agda的--type-in-type标志允许的），则可以推导出矛盾，例如这个。

这也给了我们一个简单的函数规则：

A : Set i
B : A → Set j

(a : A) → B a : Set (max i j)

将此应用于您的示例：

X   : Set
Set : Set₁

X → Set : Set (max 0 1)
X → Set : Set₁

- Vitus