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类型的A (或者在全域多态设置中的Set ℓ )都是一个命题。因此，对于某些A，A -> Set类型的P是在A的元素上定义的谓词。

例如，考虑一个谓词Positive，它只适用于某些suc n形式的自然数(我不在我的机器上，因此使用了n )：

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在很大程度上是一种符号上的便利。

至于宇宙的多态性，在旧的Agda维基中有一些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 ℓ)中。