Definition cat_of_setcategory_equalizers : Equalizers cat_of_setcategory. Proof. intros C₁ C₂ F G. use make_Equalizer. - exact (equalizer_of_setcategory F G). - exact (equalizer_of_setcategory_pr1 F G). - exact (equalizer_of_setcategory_eq F G). - use make_isEqualizer. intros C₀ H p. simple refine (_ ,, _). + refine (equalizer_of_setcategory_ump_mor F G H p ,, _). exact (equalizer_of_setcategory_ump_mor_pr1 F G H p). + abstract (simpl ; intro K ; use subtypePath ; [ intro ; apply cat_of_setcategory | ] ; apply equalizer_of_setcategory_ump_unique ; exact (pr2 K)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Setcategories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Categories.CategoryOfSetCategories. Require Import UniMath.CategoryTheory.Limits.Equalizers.