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

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

Identity type