Lemma postcompWithColimOfArrows {g : graph} (d1 d2 : diagram g C^op) (CC1 : LimCone d1) (CC2 : LimCone d2) (f : ∏ (u : vertex g), C⟦dob d1 u,dob d2 u⟧) (fNat : ∏ u v (e : edge u v), f v · dmor d2 e = (dmor d1 e : C ⟦ _ , _ ⟧) · f u) (x : C) (cc : cone d1 x) : limArrow CC1 x cc · limOfArrows CC1 CC2 f fNat = limArrow CC2 x (make_cone (λ u, coneOut cc u · f u) (postCompWithLimOfArrows_subproof CC1 CC2 f fNat x cc)). Proof. apply limArrowUnique. intro. rewrite <- assoc. rewrite limOfArrowsOut. rewrite assoc. rewrite limArrowCommutes. apply idpath. 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.Adjunctions.Core. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Import UniMath.CategoryTheory.opp_precat.