fact: Definition make_MorphismPairIsomorphism (P Q : MorphismPair) (f : z_iso (Ob1 P) (Ob1 Q)) (g : z_iso (Ob2 P) (Ob2 Q)) (h : z_iso (Ob3 P) (Ob3 Q)) : f · Mor1 Q = Mor1 P · g -> g · Mor2 Q = Mor2 P · h -> MorphismPairIsomorphism P Q := λ r s, (f,,g,,h,,(r,,!r),,(s,,!s)).
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