fact: Definition applyFunctorToPair {M N:precategory} : (M⟶N) -> @MorphismPair M -> @MorphismPair N := λ F P, make_MorphismPair (# F (Mor1 P)) (# F (Mor2 P)).
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Notations UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.Limits.Zero UniMath.CategoryTheory.Limits.Opp