Lemma images_of_fully_faithful_inv_hom_of_leg_commute₀ : # H (inv_from_z_iso i1) · pr1 α x1 · # F fx = # H fy · (# H (inv_from_z_iso i') · pr1 α px'). Proof. rewrite assoc'. etrans. { apply maponpaths. exact (! pr21 α _ _ _). } simpl. rewrite ! assoc. rewrite <- ! functor_comp. apply maponpaths_2, maponpaths. use z_iso_inv_on_left. rewrite assoc'. apply pathsinv0. use z_iso_inv_on_right. unfold fx. rewrite functor_on_fully_faithful_inv_hom. rewrite assoc'. etrans. { do 2 apply maponpaths, (z_iso_after_z_iso_inv i'). } apply id_right. 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.