Definition π₀_universal_property {X:Type} {Y:hSet} : (π₀ X -> Y) ≃ (X -> Y). Proof. exists (λ h, h ∘ component). intros f. apply iscontraprop1. - apply isaproptotal2. + intros h. use (_ : isaset _). apply impred_isaset. intros x. apply setproperty. + intros h h' e e'. apply funextsec. intro w. { apply (surjectionisepitosets component). - apply issurjsetquotpr. - apply setproperty. - intros x. exact (maponpaths (λ k, k x) (e @ ! e')). } - now exists (setquotuniv _ _ f (λ x y e, squash_to_prop e (setproperty Y (f x) (f y)) (maponpaths f))). Defined.