Lemma Cocone_postcompose {C : precategory} {g : graph} {d : diagram g C} {c : C} (cc : cocone d c) (x : C) (f : C⟦c,x⟧) : ∏ u v (e : edge u v), dmor d e · (coconeIn cc v · f) = coconeIn cc u · f. Proof. now intros u v e; rewrite assoc, coconeInCommutes. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Adjunctions.Core.