Undersand単項関係・ユニバース多型

Question

背景：私はAgdaのいくつかの基本的な理解を持っていると私はここに 主旨を理解しようとしています：

https://gist.github.com/copumpkin/5945905

をしかし、私はすべてのPredものを理解する問題を抱えています ユニバースの使用が含まれます。

これはPREDの定義です：

Pred : ∀ {a} → Set a → (ℓ : Level) → Set (a ⊔ suc ℓ) 
Pred A ℓ = A → Set ℓ 

-- Unary relations can be seen as sets 

なぜ私が今まで、このようなタイプをしたいと思うし、そのコメントが何を意味するのでしょうか？それは がどこでも使用されているので、私は本当に理解することなく進めることはできません。

位相空間のレコード定義があります、ということに続き：

record Space x ℓ : Set (Level.suc x ⊔ Level.suc ℓ) where 

この魔法は何ですか？私はxが私たちの「ポイント」のレベルであることを理解していますが、 ですが、ℓとその結果のタイプは何ですか？

Answer 1

バイナリリレーションに関するa related questionがありました。

Curry–Howard interpretationの下では、タイプSet（または、宇宙の多形性設定においてSet ℓ）の各Aが提案される。したがって、AのタイプA -> SetのPは、Aの要素で定義される述語です。

いくつかのn（私はそれゆえ私のマシンのうちのASCIIだ）のためだけのフォームsuc nの自然数について成り立つ述語Positive：

data Positive : Nat -> Set where 
    positive : forall n -> Positive (suc n) 

positive nは（むしろ、または）Positive (suc n)の証明です。私たちはもう一つの例

data Positive : Pred Nat where 

よう Positiveの型シグネチャを書くことができます Pred A = A -> Set持つことは、標準ライブラリに Data.List.Allモジュールから Allです。

data All {a p} {A : Set a} 
     (P : A → Set p) : List A → Set (p ⊔ a) where 
    [] : All P [] 
    _∷_ : ∀ {x xs} (px : P x) (pxs : All P xs) → All P (x ∷ xs) 

All PがPは、リストの各要素のために保持している時はいつでも任意のリストxsのために保持している述語であるように定義です。 Predの宇宙多型定義を使用して、我々は

data All {a p} {A : Set a} 
     (P : Pred A p) : Pred (List A) (p ⊔ a) where 

として Allの型シグネチャを書き込み（及びそれを明確 Allが述語変圧器であることを確認）することができます。したがって、 Predは、ほとんどの表記の便利さです。

宇宙多形性については、古いAgda wikiにdocsがあります。あなたの例では、xは、ポイントのタイプ（X）がある宇宙のレベルです。そのℓは、Xの要素に定義されている述語に定義されている述語のタイプ（この式の位相的意味についてはコメントできません）で使用されています（Pred (Pred X ℓ) ℓ）。 Set xは、Set (suc x)およびPred (Pred X ℓ) ℓ（(X -> Set ℓ) -> Set ℓに展開されている）にあり、Set (suc ℓ)にあり、従ってSpace x ℓはSet (suc x ⊔ suc ℓ)にあります。