Lemma images_of_fully_faithful_inv_hom_of_f₁'_commute : # H f₁' · (# H (inv_from_z_iso iy) · α y) = # H (inv_from_z_iso ix) · α x · # F f₁. Proof. refine (assoc _ _ _ @ _). rewrite <- functor_comp. refine (_ @ assoc _ _ _). etrans. 2: apply maponpaths, (pr21 α _ _ f₁). simpl. rewrite assoc. apply maponpaths_2. rewrite <- functor_comp. apply maponpaths. unfold f₁. rewrite functor_on_fully_faithful_inv_hom. rewrite ! assoc. apply maponpaths_2. refine (! id_left _ @ _). apply maponpaths_2. apply pathsinv0, z_iso_after_z_iso_inv. 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.Equalizers. Require Import UniMath.CategoryTheory.Limits.Preservation. Require Import UniMath.CategoryTheory.WeakEquivalences.Reflection.Equalizers. Require Import UniMath.CategoryTheory.WeakEquivalences.Preservation.Equalizers.