Hierarchia typów w Agdzie

Question

Próbuję dowiedzieć się, jak działają hierarchie typów w Agdzie.

Zakładając I zdefiniować zestaw wpisz X:

X : Set 

, a następnie przystąpić do konstruowania typu indukcyjnego

data Y : X -> Set where 

Jaki jest rodzaj X -> Set? Czy to jest zestaw czy typ?

Dziękujemy!

Answer 1

Dlaczego nie zapytać samej Agdy? Zamierzam użyć znakomitego trybu Agdy dla Emacsa. Zaczynamy od:

module Hierarchy where 

postulate 
    X : Set 

data Y : X → Set where 
    -- empty 

Musimy załadować plik za pomocą C-c C-l; ten typ sprawdza plik, zamienia się w otwory, zmienia podświetlanie składni i tak dalej.

Teraz jest komenda „wywnioskować (wywnioskować) typu” dostępne za pośrednictwem C-c C-d, więc użyjmy że:

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

Prawo, które ma sens. Zdefiniowaliśmy Y : X → Set, więc nie powinno to być zaskoczeniem. Zapytajmy ponownie:

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

Tak, masz go: Y : X → Set : Set₁.

---

Podczas gdy pierwsza część odpowiada na pytanie i pokazuje, jak samemu sprawdzić te rzeczy, to za każdym razem byłoby to nudne, przynajmniej. Oto jak to działa:

Aby uniknąć paradoksów, wymagamy

Set i : Set (i + 1) 

co daje Ci (nieskończone) hierarchię Set s. Jeśli miałbyś Set : Set (który Agda zezwala poprzez flagę --type-in-type), możesz wyprowadzić sprzeczność, taką jak this one.

To daje nam również prostą regułę dla funkcji:

A : Set i 
B : A → Set j 

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

stosujące niniejszy do PRZYKŁAD:

X : Set 
Set : Set₁ 

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