Lemma weak_equiv_lifts_preserves_equalizers : preserves_equalizer H. Proof. intros x' y' a' f₁' f₂' e' r Fr iEe. use (factor_through_squash _ _ (eso_from_weak_equiv _ Gw x')). { apply isaprop_isEqualizer. } intros [x ix]. use (factor_through_squash _ _ (eso_from_weak_equiv _ Gw y')). { apply isaprop_isEqualizer. } intros [y iy]. use (factor_through_squash _ _ (eso_from_weak_equiv _ Gw a')). { apply isaprop_isEqualizer. } intros [a ia]. exact (equalizer_is_preserved_after_lift iEe ix iy ia Fr). 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.