Lemma multispan_cocone_commutes {J : category} {X : UU} {d : diagram (multispan_graph X) J} {apex : J} (cc : cocone d apex) (z : X) : (dmor d (multispan_edge z)) · coconeIn cc (multispan_vertex z) = coconeIn cc multispan_base. Proof. exact(coconeInCommutes cc multispan_base (multispan_vertex z) tt). Qed.
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.