Lemma equalizer_is_preserved_after_lift (Fr : # H e' · # H f₁' = # H e' · # H f₂') : isEqualizer (# H f₁') (# H f₂') (# H e') Fr. Proof. set (αi := nat_z_iso_inv α). use (isEqualizerUnderIso _ _ _ _ _ _ _ (Feq x y a f₁ f₂ e fully_faithful_inv_hom_of_equalizer_diagram_commutes (Equalizers.p_func (p := fully_faithful_inv_hom_of_equalizer_diagram_commutes)) _)). - use (z_iso_comp (_ ,, pr2 αi _)) ; simpl ; apply functor_on_z_iso. exact ia. - use (z_iso_comp (_ ,, pr2 αi _)) ; simpl ; apply functor_on_z_iso. exact ix. - use (z_iso_comp (_ ,, pr2 αi _)) ; simpl ; apply functor_on_z_iso. exact iy. - exact (! images_of_fully_faithful_inv_hom_of_equalizer_map_commute). - exact images_of_fully_faithful_inv_hom_of_f₁'_commute. - exact images_of_fully_faithful_inv_hom_of_f₂'_commute. - exact fully_faithful_inv_hom_of_equalizer_is_equalizer. Defined.
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.