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

Question

在Agda中,a的类型forall以这样的方式确定:以下都具有类型Set1(where Set1的类型Set和A类型Set):

Set ? A
A ? Set
Set ? Set

但是,以下类型Set:

A ? A

我明白,如果Set有类型Set,就会有矛盾,但我没有看到,如果上述三个术语中的任何一个有类型Set,我们就会有矛盾.那些可以用来证明是假的吗？它们可以用来表明Set : Set吗？

Answer 1

显然Set : Set会引起矛盾,比如拉塞尔的悖论.

现在考虑() -> Set在那里()是一个单位类型.这显然是同构的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,但直觉上这似乎比其他人更有问题,也许别人会知道.

Answer 2

我认为理解这一点的最好方法是考虑这些东西是什么样的集合理论集,而不是像Agda Set.假设你有A = {a,b,c}.函数的一个例子f : A ? A是一组对,假设f = { (a,a) , (b,b) , (c,c) }它满足一些对于这个讨论无关紧要的属性.也就是说,f's元素与元素相同A- 它们只是价值观或价值观,没有太大的"大".

现在考虑一个函数F : A ? Set.它也是一组对,但它们看起来不同:F = { (a,A) , (b,Nat) , (c,Bool) }让我们说.每对的第一个元素只是一个元素A,所以它很简单,但每对的第二个元素是一个Set!也就是说,第二个元素本身就是一个"大"的东西.所以A ? Set不可能设置,因为如果是,那么我们应该能够有一些G : A ? Set看起来像G = { (a,G) , ... }.一旦我们能够做到这一点,我们就能得到拉塞尔的悖论.所以我们说A ? Set : Set1.

这也解决了是否Set ? A也应该Set1代替的问题Set,因为函数in Set ? A就像函数一样A ? Set,除了As在右边,Sets在左边,对.