Definition make_isEqualizer {a b : C} (f g : C⟦a, b⟧) (d : C) (h : C⟦d, a⟧) (H : h · f = h · g) : (∏ e (h' : C⟦e, a⟧) (H' : h' · f = h' · g), iscontr (total2 (fun hk : C⟦e, d⟧ => hk · h = h'))) -> isEqualizer f g d h H. Proof. intros H' x cx. assert (H1 : coneOut cx One · f = coneOut cx One · g). { use (pathscomp0 (coneOutCommutes cx One Two (ii1 tt))). use (pathscomp0 _ (!(coneOutCommutes cx One Two (ii2 tt)))). apply idpath. } set (H2 := (H' x (coneOut cx One) H1)). use tpair. - use (tpair _ (pr1 (pr1 H2)) _). use two_rec_dep. + apply (pr2 (pr1 H2)). + use (pathscomp0 _ (coneOutCommutes cx One Two (ii1 tt))). change (coneOut (Equalizer_cone f g d h H) (● 1)%stn) with (h · f). rewrite assoc. apply cancel_postcomposition, (pr2 (pr1 H2)). - abstract (intro t; apply subtypePath; [ intros y; apply impred; intros t0; apply hs | induction t as [t p]; apply path_to_ctr, (p One)]). 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.