proposition: Lemma limOfArrowsOut {J C : precategory} {F1 F2 : functor J C} (CC1 : LimCone F1) (CC2 : LimCone F2) (f : ∏ u, C⟦F1 u,F2 u⟧) (fNat : ∏ u v (e : J⟦u,v⟧), f u · # F2 e = # F1 e · f v) : ∏ u, limOfArrows CC1 CC2 f fNat · limOut CC2 u = limOut CC1 u · f u.
proof: Proof. now unfold limOfArrows; intro u; rewrite limArrowCommutes. Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Propositions UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.FunctorCategory