Lemma images_of_fully_faithful_inv_hom_of_equalizer_map_commute : is_z_isomorphism_mor (pr2 α a) · # H ia · # H e' · (# H (inv_from_z_iso ix) · α x) = # F e. Proof. etrans. { apply maponpaths_2. rewrite assoc'. apply maponpaths. apply pathsinv0, (functor_comp H). } etrans. { rewrite assoc. apply maponpaths_2. rewrite assoc'. apply maponpaths. apply pathsinv0, (functor_comp H). } refine (assoc' _ _ _ @ _). use (z_iso_inv_on_right _ _ _ (_ ,, pr2 α a)). simpl. refine (_ @ pr21 α _ _ _). apply maponpaths_2. simpl; apply maponpaths. unfold e. apply pathsinv0. apply functor_on_fully_faithful_inv_hom. 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.