This is an old revision of the document!
Set . HoTT
Type
$isSet(A):={\large\Pi}_{x,y:A}\,isProp(Id_A(x,y))$
Discussion
Elaboration
See the last lines of univalence axiom.
Alternative definitions
$isSet(A):={\large\Pi}_{x,y:A}{\large\Pi}_{p,q:Id_A(x,y)}\,Id_{Id_A(x,y)}(p,q)$
Reference
Parents
Requirements
