===== 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]]