Mere proposition

Type

$isProp(A):={\large\Pi}_{x,y:A}\,Id_A(x,y)$

Discussion

In HoTT, a type is a proposition iff all its terms are equal. Roughly, this means it has zero or one term.

Reference

Parents

Requirements

Identity type