在 Agda 中， a 的类型以如下方式forall确定：Set1Set1SetASet
Set → A
A → Set
Set → Set
但是，以下具有类型Set：
A → A
我知道如果Set有 type Set，会有矛盾，但我看不出，如果上述三个术语中的任何一个有 type Set，我们就会有矛盾。这些可以用来证明False吗？它们可以用来证明Set : Set吗？
问问题
1085 次
2 回答
18
很明显，这Set : Set会引起矛盾，比如罗素悖论。
现在考虑() -> Setwhere()是unit type。这显然与 同构Set。所以若然() -> Set : Set也Set : Set。事实上，如果A我们有任何有人居住，A -> Set : Set那么我们可以使用一个常量函数：SetA -> 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，但直觉上这似乎比其他类型更有问题，也许其他人会知道。
于 2012-09-23T13:13:01.470 回答
7
我认为理解这一点的最佳方法是将这些事物视为集合论集合，而不是 Agda Set。假设你有A = {a,b,c}. 函数的一个示例f : A → A是一组对，假设f = { (a,a) , (b,b) , (c,c) }它满足一些对本次讨论无关紧要的属性。也就是说，f' 元素与 ' 元素是同一类东西A——它们只是值，或者成对的值，没有什么太大的“大”。
现在考虑 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也应该 inSet1而不是 的问题Set，因为 in 中的函数与Set → A中的函数一样A → Set，只是As 在对的右边，Sets 在左边。
于 2012-09-25T21:17:29.070 回答