Wiki. 命题 (同伦类型论) [命题(同伦类型论)]
Wiki. 命题 (同伦类型论) [命题(同伦类型论)]
定义
在同伦类型论中, 称类型 $A$ 是命题, 是指 $A$ 的任意两个元素都相等, 即 $$ \mathsf{isProp}(A) := \prod_{x,y : A} x =_A y. $$
性质
对于命题 $A$, 若 $A$ 有一个元素, 那么 $A$ 可缩.
在同伦类型论中, 称类型 $A$ 是命题, 是指 $A$ 的任意两个元素都相等, 即 $$ \mathsf{isProp}(A) := \prod_{x,y : A} x =_A y. $$
对于命题 $A$, 若 $A$ 有一个元素, 那么 $A$ 可缩.