Definition make_pair_cocone {J : category} {X : UU} (d : diagram pair_graph J) (j : J) (src_in : J⟦dob d pair_src, j⟧) (dst_in : J⟦dob d pair_dst, j⟧) (com_left : dmor d pair_left · dst_in = src_in) (com_right : dmor d pair_right · dst_in = src_in) : cocone d j. Proof. use make_parallell_cocone. - exact src_in. - exact dst_in. - abstract(use coprod_rect; apply unit_rect; assumption). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Combinatorics.FiniteSets.