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