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. exact(coconeInCommutes cc parallell_start parallell_end (parallell_edge x)). 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.