(usual formulation in type theory) is equivalent to its relational
formulation (only formulation of set theory) + the axiom of
(parametric) definite description (aka axiom of unique choice) *)
(usual formulation in type theory) is equivalent to its relational
formulation (only formulation of set theory) + the axiom of
(parametric) definite description (aka axiom of unique choice) *)