Wiki. “集合 (同伦类型论)” [集合(同伦类型论)]
Wiki. “集合 (同伦类型论)” [集合(同伦类型论)]
#同伦类型论
定义
在同伦类型论中, 若类型 $A$ 满足对任意 $x,y\colon A$, 任意 $p,q\colon x=y$, 都有 $p=q$, 则称 $A$ 为集合.
例
单点 (同伦类型论)是集合.
#同伦类型论
在同伦类型论中, 若类型 $A$ 满足对任意 $x,y\colon A$, 任意 $p,q\colon x=y$, 都有 $p=q$, 则称 $A$ 为集合.
单点 (同伦类型论)是集合.