Lemma CoproductArrow_diagram (Hti : I → Signature_category C D D') (Ht : Signature C D D') (F : ∏ i : I, SignatureMor C D D' (Hti i) Ht) X Y : Signature_category_mor_diagram C D D' (Sum_of_Signatures I C D D' CD Hti) Ht (CoproductArrow I _ (CCD _) (λ i, pr1 (F i))) X Y. Proof. apply Signature_category_mor_diagram_pointwise; intro c. etrans; [apply precompWithCoproductArrow|]. apply pathsinv0, CoproductArrowUnique; intro i; rewrite assoc; simpl. etrans; [apply cancel_postcomposition, (CoproductInCommutes _ _ _ (CD (λ j, pr1 (pr1 (pr1 (Hti j)) X) _)))|]. apply pathsinv0; etrans; [apply (nat_trans_eq_pointwise (pr2 (F i) X Y) c)|]. now etrans; [apply cancel_postcomposition, horcomp_id_left|]. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.PointedFunctors. Require Import UniMath.CategoryTheory.PointedFunctorsComposition. Require Import UniMath.CategoryTheory.HorizontalComposition. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.SubstitutionSystems.Notation. Require Import UniMath.SubstitutionSystems.Signatures. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.SIP. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.SubstitutionSystems.BinProductOfSignatures. Require Import UniMath.SubstitutionSystems.SumOfSignatures.