Lemma π₀_universal_map_uniq {X:Type} {Y:hSet} (h h' : π₀ X -> Y) : (∏ x, h (component x) = h' (component x)) -> h ~ h'. Proof. intros e x. apply (surjectionisepitosets component). - apply issurjsetquotpr. - apply setproperty. - exact e. Defined.