Definition make_multispan_cocone {J : category} {X : UU} (d : diagram (multispan_graph X) J) (apex : J) (base_inject : J⟦ dob d multispan_base, apex ⟧) (inject : ∏ (x : X), J⟦ dob d (multispan_vertex x), apex ⟧) (commutes : ∏ (x : X), dmor d (multispan_edge x) · inject x = base_inject) : cocone d apex. Proof. use make_cocone. - apply coprod_rect. + exact inject. + apply unit_rect. exact base_inject. - abstract(use coprod_rect; [exact(λ _ _, empty_rect _) | use unit_rect ]; use coprod_rect; cbn; [exact(λ a, unit_rect _ (commutes a)) |exact(λ _, empty_rect _)]). 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.