Agda中的類型層次結構

Question

我想知道如何在Agda中使用類型層次結構。

假設我定義一組類型X：

X : Set 

，然後進行構建的感應型

data Y : X -> Set where 

什麼是X -> Set類型？它是設置還是類型？

謝謝！

Answer 1

那麼，爲什麼不問Agda本身？我將爲Emacs使用優秀的Agda模式。我們先從：

module Hierarchy where 

postulate 
    X : Set 

data Y : X → Set where 
    -- empty 

我們必須加載使用C-c C-l文件;這個類型檢查文件，將?寫入漏洞，語法突出顯示等等。

現在，有一個命令通過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 S上（無限）的層次結構。如果您有Set : Set（Agda允許通過--type-in-type標誌），則可能導致矛盾，如this one。

這也爲我們提供了一個功能簡單的規則：

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₁