fact: Definition make_discrete_cocone {J : category} {X : UU} (d : diagram (discrete_graph X) J) (z : J) (f : ∏ (x : X), J⟦dob d x, z⟧) : cocone d z.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.FiniteSets