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)$