Lemma inv_of_pullback_second_projection_commutes_with_image_modulo_isos : # G π₂x · i2 = i · π₂y. Proof. unfold π₂x. rewrite functor_on_fully_faithful_inv_hom. rewrite ! assoc'. apply maponpaths. refine (_ @ id_right _). apply maponpaths. apply (pr2 i2). 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.