Definition applyFunctorToPairIsomorphism {M N:precategory} (F : M⟶N) (P Q : @MorphismPair M) : MorphismPairIsomorphism P Q -> MorphismPairIsomorphism (applyFunctorToPair F P) (applyFunctorToPair F Q). Proof. intros [i1 [i2 [i3 [[d d'][e e']]]]]. exists (functor_on_z_iso F i1). exists (functor_on_z_iso F i2). exists (functor_on_z_iso F i3). repeat split. - refine (! _ @ (maponpaths (# F) d ) @ _);apply functor_comp. - refine (! _ @ (maponpaths (# F) d') @ _);apply functor_comp. - refine (! _ @ (maponpaths (# F) e ) @ _);apply functor_comp. - refine (! _ @ (maponpaths (# F) e') @ _);apply functor_comp. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.Limits.Zero. Require Import UniMath.CategoryTheory.Limits.Opp.