Definition InverseMorphismPairIsomorphism {P Q : MorphismPair} : MorphismPairIsomorphism P Q -> MorphismPairIsomorphism Q P. Proof. intros f. exists (z_iso_inv (pr1 f)). exists (z_iso_inv (pr12 f)). exists (z_iso_inv (pr122 f)). split. - split. + apply reverseCommIsoSquare. exact (pr11 (pr222 f)). + apply reverseCommIsoSquare'. exact (pr21 (pr222 f)). - split. + apply reverseCommIsoSquare. exact (pr12 (pr222 f)). + apply reverseCommIsoSquare'. exact (pr22 (pr222 f)). 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.