Definition make_parallell_cocone {J : category} {X : UU} (d : diagram (parallell_graph X) J) (z : J) (in₀ : dob d (stnpr 0) --> z) (in₁ : dob d (stnpr 1) --> z) (commutes : ∏ (x : X), dmor d (x : @edge (parallell_graph X) (stnpr 0) (stnpr 1)) · in₁ = in₀) : cocone d z. Proof. use make_cocone. - exact(two_rec_dep _ in₀ in₁). - abstract(use(two_rec_dep _ (two_rec_dep _ (empty_rect _) commutes)); exact(λ _, empty_rect _)). Defined.
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.