Definition Equalization {C:category} {c d:C} (f g:c-->d) : C^op ⟶ SET. Proof. unshelve refine (makeFunctor_op _ _ _ _). - intro b. unshelve refine (_,,_). + exact (∑ p:b --> c, f∘p = g∘p). + abstract (apply isaset_total2; [ apply homset_property | intro; apply isasetaprop; apply homset_property]) using _L_. - intros b a e w; simpl in *. exists (pr1 w ∘ e). abstract (rewrite <- 2? assoc; apply maponpaths; exact (pr2 w)) using _M_. - abstract ( intros b; apply funextsec; intro w; apply subtypePath; [ intro; apply homset_property | simpl; apply id_left]) using _N_. - abstract ( intros a'' a' a r s; apply funextsec; intro w; apply subtypePath; [ intro; apply homset_property | apply pathsinv0, assoc ]) using _O_. Defined.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import Require Import Require Import UniMath.MoreFoundations.Tactics.