Phân cấp loại trong Agda

Question

Tôi đang cố gắng tìm hiểu cách phân cấp loại hoạt động trong Agda.

Giả sử tôi định nghĩa một kiểu tập X:

X : Set 

và sau đó tiến tới xây dựng một kiểu quy nạp

data Y : X -> Set where 

loại X -> Set là gì? Là nó đặt hoặc loại?

Cảm ơn bạn!

Answer 1

Vâng, tại sao không hỏi chính Agda? Tôi sẽ sử dụng chế độ Agda tuyệt vời cho Emacs. Chúng tôi bắt đầu với:

module Hierarchy where 

postulate 
    X : Set 

data Y : X → Set where 
    -- empty 

Chúng tôi phải tải tệp bằng cách sử dụng C-c C-l; điều này đánh máy tập tin, biến ? s thành lỗ, làm nổi bật cú pháp và như vậy.

Bây giờ, có một lệnh "Suy luận (suy ra) gõ" có sẵn thông qua C-c C-d, vì vậy hãy sử dụng:

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

Phải, có ý nghĩa. Chúng tôi đã xác định Y : X → Set, vì vậy sẽ không có gì ngạc nhiên. Hãy hỏi lại:

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

Vì vậy, bạn có nó: Y : X → Set : Set₁.

---

Trong khi phần đầu trả lời câu hỏi và cho bạn biết cách tự kiểm tra nội dung này, hãy làm điều đó mọi lúc sẽ ít ỏi. Dưới đây là cách hoạt động:

Để tránh những nghịch lý, chúng tôi yêu cầu

Set i : Set (i + 1) 

mà cung cấp cho bạn (vô hạn) hệ thống các Set s. Nếu bạn có Set : Set (mà Agda cho phép qua cờ --type-in-type), bạn có thể lấy được mâu thuẫn như this one.

này cũng cho chúng ta một nguyên tắc đơn giản cho các chức năng:

A : Set i 
B : A → Set j 

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

Áp dụng điều này để ví dụ của bạn:

X : Set 
Set : Set₁ 

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