Lemma fully_faithful_inv_hom_of_equalizer_is_equalizer : isEqualizer f₁ f₂ e fully_faithful_inv_hom_of_equalizer_diagram_commutes. Proof. use (weak_equiv_reflects_equalizers Gw). use (isEqualizerUnderIso _ _ _ _ _ _ _ iEe). - exact (z_iso_inv ia). - exact (z_iso_inv ix). - exact (z_iso_inv iy). - exact inv_of_equalizer_map_commutes_with_image_modulo_isos. - exact inv_of_f₁'_commutes_with_image_modulo_isos. - exact inv_of_f₂'_commutes_with_image_modulo_isos. 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.