Wiki. 可缩类型 (同伦类型论) [可缩(同伦类型论)]
Wiki. 可缩类型 (同伦类型论) [可缩(同伦类型论)]
定义
在同伦类型论中, 称类型 $A$ 可缩, 是指 $A$ 有元素 $a: A$ 使得 $A$ 的任意元素都等于 $a$, 即 $$ \mathsf{isContr}(A) := \sum_{a : A}\prod_{x : A} x =_A a. $$
在同伦类型论中, 称类型 $A$ 可缩, 是指 $A$ 有元素 $a: A$ 使得 $A$ 的任意元素都等于 $a$, 即 $$ \mathsf{isContr}(A) := \sum_{a : A}\prod_{x : A} x =_A a. $$