Lemma weak_equiv_lifts_preserves_chosen_equalizers_eq : preserves_chosen_equalizers_eq H E₂ E₃. Proof. intros x' y' f' g'. use (factor_through_squash _ _ (eso_from_weak_equiv _ Gw x')). { apply isapropishinh. } intros [x ix]. use (factor_through_squash _ _ (eso_from_weak_equiv _ Gw y')). { apply isapropishinh. } intros [y iy]. pose (j1 := isotoid _ (pr2 C2) ix). pose (j2 := isotoid _ (pr2 C2) iy). induction j1. induction j2. exact (lift_preserves_chosen_equalizers_uptoeq_after_isotoid_induction f' g'). 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.