宇宙是什么意思？

Question

有关函数式编程的文章，其中很多都提到了Universe。我正在阅读Bartosz Milewski的著作《程序员的类别理论》，他也多次提到宇宙。问题是，在函数式编程和范畴论的语境中，宇宙意味着什么？

Answer 1

在范畴论的背景下，引入了宇宙以绕开集合论的悖论。例如，Set是集合的类别，因此其对象对应于集合。此类别中所有对象的集合就是所有集合的集合。但是没有所有的一套！格洛腾迪克介绍了宇宙的概念来解决这一问题。本质上，给定Universe中的所有集合都不是该Universe中的集合，而是下一个更大Universe中的集合。

在编程中，我们必须处理多态函数，即为所有类型定义的函数。但是，所有类型都不构成集合。因此，诸如Agda之类的语言使您可以处理给定Universe中的类型。它们称为最低的Universe集，但是Set本身是Set ₁的成员，依此类推。