Definition equiv_Equalizers2 : @Limits.Equalizers.Equalizers C <- Equalizers C. Proof. intros E' a b f g. set (E := E' a b f g). exact (@Limits.Equalizers.make_Equalizer C (EqualizerObject C E) a b f g (EqualizerArrow C E) (EqualizerArrowEq C E) (@equiv_isEqualizer2 a b f g (EqualizerObject C E) (EqualizerArrow C E) (EqualizerArrowEq C E) (isEqualizer_Equalizer C 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.