Corollary weak_equiv_preserves_equalizers_eq {C D : category} {F : C ⟶ D} (Fw : is_weak_equiv F) (Duniv : is_univalent D) (E₁ : Equalizers C) (E₂ : Equalizers D) : preserves_chosen_equalizers_eq F E₁ E₂. Proof. intros x y f g. apply hinhpr. apply Duniv. set (Fe := weak_equiv_preserves_equalizers Fw). set (e₂ := (E₂ _ _ (#F f) (#F g))). use (z_iso_from_Equalizer_to_Equalizer (make_Equalizer _ _ _ _ (Fe _ _ _ _ _ _ _ _ (pr22 (E₁ _ _ f g)))) (E₂ _ _ (#F f) (#F g)) ). do 2 rewrite <- functor_comp. apply maponpaths. apply E₁. 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.