为什么不设置 - >设置:设置？

Question

在Coq作为一名数学家,我本来期待的

Set -> Set : Set

但我想这是因为我的数学家帽子已经开启了.我该怎么做才能让它发挥作用？

我是否应该考虑设置不同并使用不同类型的Set？

Answer 1

我想这是因为我的数学家帽子已经开启了

也许你需要你的理论帽子.我们可以Set -> (Set -> Set)通过将每个Set函数发送到返回的常量函数来构建注入Set,即fun S => (fun _ => S).如果(Set -> Set) : Set,那么我们将有一个(Set -> Set)包含所有集合的集合(即).这将是一个问题,因为那时你可以跟随拉塞尔的悖论并询问所有不包含自己的集合的集合,你可以问这个集合是否包含自己,这是荒谬的.因此,你不能拥有(Set -> Set) : Set.(另见Coq.Logic.Hurkens该定理变体的形式化版本.)

因为(Set -> Set)太大而不能成为一个Set,所以它生活在下一个层次上Type.它可能会有所帮助Set Printing Universes.一般来说,我们有Type@{i} : Type@{i+1}.