proposition: Lemma parallell_cocone_commutes {J : category} {X : UU} {d : diagram (parallell_graph X) J} {j : J} (cc : cocone d j) (x : X) : dmor d (parallell_edge x) · coconeIn cc parallell_end = coconeIn cc parallell_start.
proof: Proof. exact(coconeInCommutes cc parallell_start parallell_end (parallell_edge x)). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.FiniteSets