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

定义

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

例

单点是集合.