Definition make_isCoequalizer {a b : C} (f g : C⟦a, b⟧) (d : C) (h : C⟦b, d⟧) (H : f · h = g · h) : (∏ e (h' : C⟦b, e⟧) (H' : f · h' = g · h'), iscontr (total2 (fun hk : C⟦d, e⟧ => h · hk = h'))) -> isCoequalizer f g d h H. Proof. intros H' x cx. assert (H1 : f · coconeIn cx Two = g · coconeIn cx Two). { use (pathscomp0 (coconeInCommutes cx One Two (ii1 tt))). use (pathscomp0 _ (!(coconeInCommutes cx One Two (ii2 tt)))). apply idpath. } set (H2 := (H' x (coconeIn cx Two) H1)). use tpair. - use (tpair _ (pr1 (pr1 H2)) _). use two_rec_dep. + use (pathscomp0 _ (coconeInCommutes cx One Two (ii1 tt))). change (coconeIn (Coequalizer_cocone f g d h H) _) with (f · h). change (dmor _ _) with f. rewrite <- assoc. apply cancel_precomposition, (pr2 (pr1 H2)). + apply (pr2 (pr1 H2)). - abstract (intro t; apply subtypePath; [intros y; apply impred; intros t0; apply C |induction t as [t p]; apply path_to_ctr, (p Two)]). 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.Functors. 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.Graphs.EqDiag. Require Import UniMath.CategoryTheory.Limits.Coequalizers.