宇宙是什么意思？

Question

关于函数式编程的文章，很多都提到了宇宙。 我正在阅读 Bartosz Milewski 的《程序员类别理论》一书，他也多次提到宇宙。 问题是，在函数式编程和范畴论的背景下，宇宙意味着什么？

Answer 1

在范畴论的背景下，引入宇宙是为了绕过集合论的悖论。例如，Set 是集合的范畴，所以它的对象对应于集合。此类别中所有对象的集合将是所有集合的集合。但是没有所有集合的集合！ Grothendieck 引入了宇宙的概念来解决这个问题。本质上，给定宇宙中所有集合的集合不是该宇宙中的集合——它是下一个更大宇宙中的集合。

在编程中，我们必须处理多态函数，即为所有类型定义的函数。但并非所有类型都形成一个集合。所以像Agda 这样的语言可以让你在给定的宇宙中使用类型。他们称最低宇宙 Set，但 Set 本身是 Set₁ 的成员，以此类推。