Definition weak_equiv_into_univ_creates_equalizers {C1 C2 : category} (C2_univ : is_univalent C2) {F : C1 ⟶ C2} (Fw : is_weak_equiv F) (E₁ : Equalizers C1) : Equalizers C2.
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.Preservation.Equalizers. Require Import UniMath.CategoryTheory.WeakEquivalences.Reflection.Equalizers.