Tür Hiyerarşi

Question

Agda'da tür hiyerarşilerinin nasıl çalıştığını anlamaya çalışıyorum.

X : Set 

ve sonra bir endüktif tip

data Y : X -> Set where 

X -> Set türü nedir inşa geçin:

Bir set tipi X tanımlamak varsayarsak? Set mi, Tip mi?

Teşekkür ederiz!

Answer 1

Peki, neden Agda'nın kendisine sormuyorsunuz? Emacs için mükemmel Agda modunu kullanacağım. Biz C-c C-l kullanarak dosyayı yüklemek zorunda

module Hierarchy where 

postulate 
    X : Set 

data Y : X → Set where 
    -- empty 

;: ile başlıyoruz Bu typechecks dosyayı, ? s deliklere çevirir, sözdizimi vurgulama yapar ve böyle devam eder.

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

Sağ, mantıklıdır:

Şimdi, bir komut C-c C-d yoluyla ulaşılabilir "Infer (anlamak) tipi", öyleyse o kullanmasına izin yoktur. Y : X → Set'u tanımladık, bu yüzden sürpriz olmamalı. Tekrar soralım:

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

Yani, orada o var: Y : X → Set : Set₁. İlk bölüm soruya cevap verir ve en az, donuk olacağını her şey yapıyor, bu malzeme kendini nasıl kontrol edileceğini gösterir iken

---

. Burada şöyle çalışır:

paradokslar önlemek için, size Set s (sonsuz) hiyerarşiyi verir

Set i : Set (i + 1) 

gerektirir. Set : Set (Agda'nın --type-in-type bayrağıyla izin verdiği durumlarda) varsa, this one gibi çelişkileri türetebilirsiniz.

A : Set i 
B : A → Set j 

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

örneğinize buna uygulamak:

X : Set 
Set : Set₁ 

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