Definition limit_of_coproduct_as_cone_of_coproduct_to_limit : cone coproduct_n_cochain coproduct_of_limit. Proof. use tpair. - intro n. use CoproductOfArrows. exact (λ i, coneOut (limCone (ω_lim_given (ind i))) n). - intros n m p. cbn. etrans. 1: apply precompWithCoproductArrow. use CoproductArrowUnique. intro i. etrans. 1: apply (CoproductInCommutes _ _ _ coproduct_of_limit _ (λ i0 : I, coneOut (limCone (ω_lim_given (ind i0))) n · (dmor (ind i0) p · CoproductIn I C (coproducts_given (λ i1 : I, dob (ind i1) m)) i0))). etrans. 1: apply assoc. apply maponpaths_2. exact (coneOutCommutes (limCone (ω_lim_given (ind i))) n m p). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.Combinatorics.Lists. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.FunctorAlgebras. Require Import UniMath.CategoryTheory.exponentials. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Chains.All. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Categories.HSET.Limits. Require Import UniMath.CategoryTheory.Categories.HSET.Colimits. Require Import UniMath.CategoryTheory.Categories.HSET.Structures. Require Import UniMath.CategoryTheory.Categories.StandardCategories. Require Import UniMath.CategoryTheory.Groupoids. Require Import UniMath.SubstitutionSystems.Signatures. Require Import UniMath.SubstitutionSystems.SumOfSignatures. Require Import UniMath.SubstitutionSystems.BinProductOfSignatures. Require Import UniMath.SubstitutionSystems.MultiSorted_alt. Require Import UniMath.CategoryTheory.Chains.OmegaContFunctors. Require Import UniMath.SubstitutionSystems.ContinuitySignature.GeneralLemmas.