Definition PushoutCocone {a b c : C} (f : C ⟦a, b⟧) (g : C⟦a, c⟧) (d : C) (f' : C ⟦b, d⟧) (g' : C ⟦c, d⟧) (H : f · f' = g · g') : cocone (pushout_diagram f g) d. Proof. use make_cocone. - use three_rec_dep; try assumption. apply (f · f'). - use three_rec_dep; use three_rec_dep. + exact (empty_rect _). + intros x; apply idpath. + intros x; apply (! H). + exact (empty_rect _). + exact (empty_rect _). + exact (empty_rect _). + exact (empty_rect _). + exact (empty_rect _). + exact (empty_rect _). 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.