Lemma inv_of_equalizer_map_commutes_with_image_modulo_isos : e' = z_iso_inv ia · # G e · pr12 (z_iso_inv ix). Proof. unfold e. rewrite functor_on_fully_faithful_inv_hom. rewrite ! assoc. rewrite z_iso_inv_after_z_iso. rewrite id_left. rewrite assoc'. apply pathsinv0. etrans. { apply maponpaths. apply (z_iso_inv_after_z_iso (z_iso_inv ix)). } 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.Equalizers. Require Import UniMath.CategoryTheory.Limits.Preservation. Require Import UniMath.CategoryTheory.WeakEquivalences.Reflection.Equalizers. Require Import UniMath.CategoryTheory.WeakEquivalences.Preservation.Equalizers.