理解一元关系和宇宙多态性

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

为什么我会想要这样的类型？那条评论是什么意思？它正在无处不在，所以我不能不理解就无法继续。

接着是拓扑space:

的记录定义

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

这是什么魔法？我有点理解 x 是我们 "points" 的水平，但是 ℓ 和结果类型是什么？

Answer 1

关于二元关系。

在Curry–Howard interpretation下，每个Set类型的A（或在宇宙多态设置中的Set ℓ）是一个命题。因此 A -> Set 类型的 P for some A 是定义在 A.

元素上的谓词

考虑例如一个谓词 Positive，它仅适用于某些 n 形式的自然数 suc n（我不在我的机器中，因此是 ASCII）：

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

positive n 是 Positive (suc n) 的（或者更确切地说，是）证明。有了 Pred A = A -> Set 我们可以将 Positive 的类型签名写成

data Positive : Pred Nat where

另一个示例是标准库中 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 的全域多态定义，我们可以将 All 的类型签名写成

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

（并明确 All 是谓词转换器）。所以 Pred 主要是符号方便。

关于 Universe 多态性，旧的 Agda wiki 中有一些 docs。在您的示例中，x 是点类型 (X) 所在的宇宙级别。在 Pred (Pred X ℓ) ℓ 中使用了 ℓ — 在 X 的元素上定义的谓词上定义的谓词类型（我无法评论此表达式的拓扑含义）。 Set x 位于 Set (suc x) 而 Pred (Pred X ℓ) ℓ （展开为 (X -> Set ℓ) -> Set ℓ）位于 Set (suc ℓ) 因此整个 Space x ℓ 位于 Set (suc x ⊔ suc ℓ) .

理解一元关系和宇宙多态性

Undersand Unary Relations and Universe polymorphism

agda