Definition AlgebrasForBincoproductIntoProductcategory_data : functor_data (FunctorAlg F) (category_binproduct (FunctorAlg F1) (FunctorAlg F2)). Proof. use make_functor_data. - intro X. split. + exists (pr1 X). exact (τ1 X). + exists (pr1 X). exact (τ2 X). - intros X X' f. split; cbn. + exists (pr1 f). abstract (unfold τ1; rewrite assoc'; etrans; [apply maponpaths; apply (pr2 f) |]; rewrite assoc; etrans; [apply cancel_postcomposition; apply BinCoproductIn1Commutes |]; apply assoc'). + exists (pr1 f). abstract (unfold τ2; rewrite assoc'; etrans; [apply maponpaths; apply (pr2 f) |]; rewrite assoc; etrans; [apply cancel_postcomposition; apply BinCoproductIn2Commutes |]; 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.