Lemma fully_faithful_inv_hom_of_equalizer_diagram_commutes : e · f₁ = e · f₂. Proof. unfold f₁, f₂, e. repeat (rewrite <- fully_faithful_inv_comp). apply maponpaths. repeat rewrite assoc'. apply maponpaths. etrans. { apply maponpaths. rewrite assoc. apply maponpaths_2. apply (pr2 ix). } etrans. { rewrite id_left. rewrite assoc. apply maponpaths_2. exact r. } rewrite assoc'. apply maponpaths. apply pathsinv0. refine (assoc _ _ _ @ _). etrans. { apply maponpaths_2. apply (pr2 ix). } apply id_left. 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.