Definition AlgebrasForCoproductIntoProductcategory_data : functor_data (FunctorAlg sF) (product_category (fun i => FunctorAlg (F i))). Proof. use make_functor_data. - intro X. intro i. exists (pr1 X). exact (taui_from_alg X i). - intros X X' f. intro i. exists (pr1 f). abstract (unfold taui_from_alg; cbn; rewrite assoc'; etrans; [apply maponpaths; apply (pr2 f) |]; rewrite assoc; etrans; [ apply cancel_postcomposition; apply (CoproductInCommutes I C (λ i0 : I, F i0 (pr1 X)) (HC (λ i0 : I, F i0 (pr1 X)))) |]; apply assoc'). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Arithmetic.NNO. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.ProductCategory. Require Import UniMath.CategoryTheory.Limits.Coproducts.