Lemma AlgebrasForCoproductIntoProductcategory_is_functor : is_functor AlgebrasForCoproductIntoProductcategory_data. Proof. split; red. - intro X. apply funextsec. intro i. transparent assert (xx : (ob (total_precategory (algebra_disp_cat (F i))))). { exists (pr1 X). exact (taui_from_alg X i). } apply (mor_eq_total_category_when_locally_prop(D:=algebra_disp_cat (F i)) (is_locally_propositional_algebra_disp_cat (F i)) (xx:=xx)(yy:=xx)). apply idpath. - intros X Y Z f g. apply funextsec. intro i. transparent assert (xx : (ob (total_precategory (algebra_disp_cat (F i))))). { exists (pr1 X). exact (taui_from_alg X i). } transparent assert (zz : (ob (total_precategory (algebra_disp_cat (F i))))). { exists (pr1 Z). exact (taui_from_alg Z i). } apply (mor_eq_total_category_when_locally_prop(D:=algebra_disp_cat (F i)) (is_locally_propositional_algebra_disp_cat (F i)) (xx:=xx)(yy:=zz)). apply idpath. Qed.
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.