fact: Definition 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 × Mor1 P · g = f · Mor1 Q ) × ( g · Mor2 Q = Mor2 P · h × Mor2 P · h = g · Mor2 Q ).
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