Definition equalizer_of_setcategory_ump_unique {C₁ C₂ : setcategory} (F G : C₁ ⟶ C₂) {C₀ : setcategory} (H : C₀ ⟶ C₁) (p : H ∙ F = H ∙ G) (K : C₀ ⟶ equalizer_of_setcategory F G) (K_pr1 : K ∙ equalizer_of_setcategory_pr1 F G = H) : K = equalizer_of_setcategory_ump_mor F G H p.
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.