Lemma inv_of_pullback_leg_gy_commutes_with_image_modulo_isos : i2 · gy = # G gx · i'. Proof. unfold gx. rewrite functor_on_fully_faithful_inv_hom. rewrite ! assoc'. apply maponpaths. refine (! id_right _ @ _). apply maponpaths, pathsinv0. apply (pr2 i'). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.WeakEquivalences.Core. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Preservation. Require Import UniMath.CategoryTheory.WeakEquivalences.Reflection.Pullbacks. Require Import UniMath.CategoryTheory.WeakEquivalences.Preservation.Pullbacks.