Wiki. 集合 (同伦类型论) [集合(同伦类型论)]

定义

在同伦类型论中, 若类型 $A$ 满足对任意 $x,y\colon A$, 任意 $p,q\colon x=y$, 都有 $p=q$, 则称 $A$ 为集合.

换言之, $A$ 是集合当且仅当 $A$ 中任意两个元素之间的等式类型都是命题.

例

单点是集合.

所有命题都是集合.