types - 为什么 (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

很明显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 做类似的事情，但直觉上这似乎比其他类型更有问题，也许其他人会知道。