proposition: 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: Proof. exact(coconeInCommutes cc multispan_base (multispan_vertex z) tt). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.FiniteSets