Definition limOfArrows {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) : C⟦lim CC1 , lim CC2⟧. Proof. apply limArrow; use make_cone. - now intro u; apply (limOut CC1 u · f u). - abstract (intros u v e; simpl; now rewrite <- assoc, fNat, assoc, limOutCommutes). Defined.
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.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.FunctorCategory.