fact: Definition π₀_map {X Y:Type} : (X -> Y) -> (π₀ X -> π₀ Y) := λ f, setquotfun (pathseqrel X) (pathseqrel Y) f (λ x x', hinhfun (maponpaths f)).
imports: UniMath.MoreFoundations.Propositions UniMath.Foundations.Sets