Lemma reverseCommIsoSquare {M : precategory} {P Q P' Q':M} (f:P'-->P) (g:Q'-->Q) (i:z_iso P' Q') (j:z_iso P Q) : i · g = f · j -> z_iso_inv i · f = g · z_iso_inv j. Proof. intros l. refine (! id_right _ @ _). refine (maponpaths _ (! is_inverse_in_precat1 (z_iso_is_inverse_in_precat j)) @ _). refine (! assoc (z_iso_inv i) _ _ @ _). refine (maponpaths _ (assoc f _ _) @ _). refine (maponpaths (precomp_with (z_iso_inv i)) (maponpaths (postcomp_with (inv_from_z_iso j)) (!l)) @ _); unfold precomp_with, postcomp_with. refine (maponpaths _ (! assoc _ _ _) @ _). refine (assoc _ _ _ @ _). refine (maponpaths (postcomp_with (g · inv_from_z_iso j)) (is_inverse_in_precat2 (z_iso_is_inverse_in_precat i)) @ _); unfold postcomp_with. exact (id_left _). Qed.
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.