===== Set . HoTT =====
==== Type ====
${\mathrm{isSet}}(A):={\large\Pi}_{x,y:A}\,isProp(Id_A(x,y))$
==== Discussion ====
=== Elaboration ===
See the last lines of [[univalence axiom]].

=== Alternative definitions ===
${\mathrm{isSet}}(A):={\large\Pi}_{x,y:A}\,{\large\Pi}_{p,q: {\mathrm {Id}}_A(x,y)}\,{\mathrm {Id}}_{{\mathrm {Id}}_A(x,y)}(p,q)$

${\mathrm{isSet}}(A):={\large\Pi}(x,y:A)\,{\large\Pi}(p,q: {\mathrm {Id}}_A(x,y))\,{\mathrm {Id}}_{{\mathrm {Id}}_A(x,y)}(p,q)$

=== Reference ===
==== Parents ====
=== Requirements ===
[[Mere proposition]]