isProp(A):=Πx,y:AIdA(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