proposition: 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: 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.
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