Agda の集合の Level

Agda の方を先に読んだ方がわかりやすいはずです。ここでは、Set n などと書く時の n について調べます。

List の定義で、集合のLevelを取っても、定義自体は問題なく受け入れられます。

    postulate A : Set  
    postulate B : Set  
    postulate C : Set  
    postulate a : A  
    postulate b : A  
    postulate c : A  
    infixr 40 _::_
    data  List (A : Set ) : Set where
       [] : List A
       _::_ : A -> List A -> List A

では、

    l1 = a :: []

問題ありませんが、

    l1' = A :: []

では、

   Set₁ != Set

と言われてしまいます。これは A が Set₁ であることを示しています。a は、宣言から Set です。

集合 (Set) の Level は

   open import Level

を使うことにより、操作することができます。Level は自然数であり、zero から suc level という形を持つ。ただの Set は Set zero です。また、

    { c₁ c₂ ℓ : Level}  Set (c₁ ⊔ c₂ ⊔ ℓ)

などのように ⊔ を使って、大きい方を取ることができます。

    infixr 40 _::_
    data  List  (A : Set (suc zero)) : Set (suc zero) where
       [] : List A
       _::_ : A -> List A -> List A

とすると、

    l1' = A :: []

は問題ありませんが、

   l1 = a :: []

は、

   Set != Set₁

と言われてしまいます。

すべてのレベルに対する List の定義

Level を含んだ List の定義は以下のようになります。

    infixr 40 _::_
    data  List {a} (A : Set a) : Set a where
       [] : List A
       _::_ : A -> List A -> List A
    infixl 30 _++_
    _++_ : ∀ {a} {A : Set a} -> List A -> List A -> List A
    []        ++ ys = ys
    (x :: xs) ++ ys = x :: (xs ++ ys)
    l1 = a :: []
    l1' = A :: []
    l2 = a :: b :: a :: c ::  []
    l3 = l1 ++ l2
    infixr 20  _==_
    data _==_ {n} {A : Set n} :  List A -> List A -> Set n where
          reflection  : {x : List A} -> x == x
          eq-cons : {x y : List A} { a : A } -> x ==  y -> ( a :: x ) == ( a :: y )
          trans-list : {x y z : List A} { a : A } -> x ==  y -> y == z -> x == z

Level は{a}という暗黙の引数 (implicit variable) で書かれます。data は「ある Level a」に対して定義されます。

append _++_ は、すべてのレベルに対して定義されています。

    _++_ : {a : Level} -> {A : Set a} -> List A -> List A -> List A

とも書きます。data の {a} に ∀ を付けることはできません。

    list-id-l : { A : Set } -> { x : List A} ->  [] ++ x == x
    list-id-l = reflection

使う場合は、Level を省略しても良い。暗黙の引数は自動的に推論されます。推論に失敗することもありますが。

Level が上がる場合

引数に異なる Level の集合が含まれる場合は、その最大値に合わせる必要があります。

    { c₁ c₂ ℓ : Level}  Set (c₁ ⊔ c₂ ⊔ ℓ)

を使います。

Level n の集合を返す関数自体は、一つ上の Level の集合である必要があります。 level-ex.agda

    module level-ex where
    open import Level
    postulate ℓ : Level
    postulate A : Set ℓ
    postulate a : A
    lemma1 : Set  ℓ -> A
    lemma1  = \x -> a
    lemma2 : A -> Set  ℓ
    lemma2 = \x -> A
    lemma3 : Set  (suc ℓ)
    lemma3 = A -> Set  ℓ

Binary Relation に、そういう例があります。

    -- Heterogeneous binary relations                                                                                                                      
    REL : ∀ {a b} → Set a → Set b → (ℓ : Level) → Set (a ⊔ b ⊔ suc ℓ)
    REL A B ℓ = A → B → Set ℓ
    -- Homogeneous binary relations                                                                                                                        
    Rel : ∀ {a} → Set a → (ℓ : Level) → Set (a ⊔ suc ℓ)
    Rel A ℓ = REL A A ℓ

Next : Agda の record 　