为什么 (Set -> Set) 不能有 Set 类型？

Question

在 Agda 中，forall 的类型是这样确定的，即以下所有的类型都是 Set1（其中 Set1 是 Set 的类型，A 的类型是 Set） ：

Set → A
A → Set
Set → Set

但是，下面的类型为Set：

A → A

我知道如果Set 的类型为Set，就会产生矛盾，但我看不出，如果上述三个术语中的任何一个具有Set 的类型，我们就会产生矛盾。这些可以用来证明False吗？它们可以用来显示Set : Set吗？

Answer 1

我认为理解这一点的最佳方法是将这些事物视为集合论集合，而不是 Agda Set。假设你有A = {a,b,c}。函数f : A → A 的一个示例是一组对，比如说f = { (a,a) , (b,b) , (c,c) }，它满足一些与本讨论无关的属性。也就是说，f 的元素与A 的元素是同一类东西——它们只是值，或者成对的值，没有什么太大的“大”。

现在考虑一个函数F : A → Set。它也是一组对，但它的对看起来不同：F = { (a,A) , (b,Nat) , (c,Bool) } 可以说。每对的第一个元素只是A的一个元素，所以很简单，但是每对的第二个元素是一个Set！也就是说，第二个元素本身就是一个“大”的东西。所以不可能设置A → Set，因为如果是这样，那么我们应该能够有一些看起来像G = { (a,G) , ... } 的G : A → Set。只要我们能得到这个，我们就能得到罗素悖论。所以我们改用A → Set : Set1。

这也解决了Set → A是否也应该在Set1而不是Set中的问题，因为Set → A中的函数就像A → Set中的函数一样，除了@987654340 @s 在右边，Sets 在左边。

Answer 2

很明显Set : Set会引起矛盾，比如Russell's paradox。

现在考虑() -> Set，其中() 是unit type。这显然与Set 同构。所以如果() -> Set : Set 那么Set : Set。事实上，如果对于任何有人居住的A 我们有A -> Set : Set，那么我们可以使用一个常量函数将Set 包装成A -> Set：

wrap1 : {A : Set} -> Set -> (A -> Set)
wrap1 v = \_ -> v

并在需要时获取值

unwrap1 : {A : Set}(anyInhabitant : A) -> (A -> Set) -> Set
unwrap1 anyInhabitant f = f anyInhabitant

所以我们可以重构罗素悖论，就像我们有Set : Set一样。

---

同样适用于Set -> Set，我们可以将Set 包装成Set -> Set：

data Void : Set where

unwrap2 : (Set -> Set) -> Set
unwrap2 f = f Void

wrap2 : Set -> (Set -> Set)
wrap2 v = \_ -> v

在这里我们可以使用任何类型的Set 来代替Void。

---

我不确定如何用Set -> A 做类似的事情，但直觉上这似乎比其他类型更有问题，也许其他人会知道。