Wiki. 截断性 (同伦类型论) [截断性(同伦类型论)]

定义

在同伦类型论中, 归纳定义类型 $A$ 上的谓词 $$ \mathsf{Is}\text{-}n\text{-}\mathsf{Type}(A):= \begin{cases} \mathsf{IsContr} (A) & n=-2\\ \prod_{x,y\colon A}\mathsf{Is}\text{-}(n-1)\text{-}\mathsf{Type}(x=_A y) & n>-2. \end{cases} $$