Definition equiv_Equalizer1 {a b : C} (f g : C⟦a, b⟧) : Limits.Equalizers.Equalizer f g -> Equalizer C f g. Proof. intros E. 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.