A recent PR includes the following definition of sets.
#def is-set
( A : U)
: U
:= (x : A) → (y : A) → (p : x = y) → (q : x = y) → p = q
Apply the equivalence of various characterizations or propositions to prove that is-set is equivalent to is-0-type, which is yet to be defined, but could be defined here as a placeholder.
A recent PR includes the following definition of sets.
Apply the equivalence of various characterizations or propositions to prove that
is-setis equivalent tois-0-type, which is yet to be defined, but could be defined here as a placeholder.