Definition opp_MorphismPairIsomorphism {M:precategory} {P Q: @MorphismPair M} : MorphismPairIsomorphism P Q -> MorphismPairIsomorphism (MorphismPair_opp Q) (MorphismPair_opp P) := λ f, opp_z_iso (pr122 f),, opp_z_iso (pr12 f),, opp_z_iso (pr1 f),, (pr22 (pr222 f),,pr12 (pr222 f)),, (pr21 (pr222 f),,pr11 (pr222 f)).
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.