Definition make_isPushout {a b c d : C} (f : C ⟦a, b⟧) (g : C ⟦a, c⟧) (i1 : C⟦b, d⟧) (i2 : C⟦c, d⟧) (H : f · i1 = g · i2) : (∏ e (h : C ⟦b, e⟧) (k : C⟦c, e⟧)(Hk : f · h = g · k ), iscontr (total2 (fun hk : C⟦d, e⟧ => dirprod (i1 · hk = h)(i2 · hk = k)))) → isPushout f g i1 i2 H. Proof. intros H' x cx. unfold is_cocone_mor; simpl in *. set (H1 := H' x (coconeIn cx Two) (coconeIn cx Three)). use (let p : f · coconeIn cx Two = g · coconeIn cx Three := _ in _ ). { eapply pathscomp0; [apply (coconeInCommutes cx One Two tt)|]. apply pathsinv0, (coconeInCommutes cx One Three tt). } set (H2 := H1 p). use tpair. + exists (pr1 (pr1 H2)). use three_rec_dep. * abstract (use (pathscomp0 _ (coconeInCommutes cx One Two tt)); change (three_rec_dep _ _ _ _ _) with (f · i1); change (dmor _ _) with f; rewrite <- assoc; apply cancel_precomposition, (pr1 (pr2 (pr1 H2)))). * abstract ( apply (pr1 (pr2 (pr1 H2)))). * abstract (now use (pathscomp0 _ (pr2 (pr2 (pr1 H2))))). + abstract (intro t; apply subtypePath; [ intro; apply impred; intro; apply C | destruct t as [t p0]; apply path_to_ctr; split; [ apply (p0 Two) | apply (p0 Three) ]]). 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.Core.Univalence. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Pushouts.