Definition equiv_Equalizers1 : @Limits.Equalizers.Equalizers C -> Equalizers C. Proof. intros E' a b f g. set (E := E' a b f g). exact (make_Equalizer C f g _ _ _ (equiv_isEqualizer1 (Limits.Equalizers.EqualizerObject E) (Limits.Equalizers.EqualizerArrow E) (Limits.Equalizers.EqualizerEqAr E) (Limits.Equalizers.isEqualizer_Equalizer E))). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Equalizers.