Definition BinCoproduct_of_functors_Coproduct_of_booleanshape_of_functors {C D : category} (BC : Colims_of_shape two_graph D) (F G : functor C D) : nat_z_iso (BinCoproduct_of_functors C D (BinCoproducts_from_Colims _ BC) F G) (coproduct_of_functors bool C D (Coproducts_from_Colims _ _ BC) (λ x : bool, if x then F else G)). Proof. use make_nat_z_iso. - use make_nat_trans. + intro c. use colimOfArrows. * intro b. induction b ; apply identity. * intros b1 b2 e. apply fromempty. exact e. + intros c1 c2 f. cbn. etrans. 2: apply pathsinv0, precompWithColimOfArrows. etrans. 1: apply postcompWithColimArrow. apply colimArrowUnique. intro b. cbn. etrans. 1: apply (colimArrowCommutes (BC (bincoproduct_diagram D (F c1) (G c1)))). cbn. induction b. * cbn. etrans. 1: apply assoc'. etrans. 1: { apply maponpaths. apply (colimArrowCommutes (BC (bincoproduct_diagram D (F c2) (G c2))) _ _ true). } cbn. etrans. 1: apply maponpaths, id_left. apply pathsinv0, id_left. * cbn. etrans. 1: apply assoc'. etrans. 1: { apply maponpaths. apply (colimArrowCommutes (BC (bincoproduct_diagram D (F c2) (G c2))) _ _ false). } cbn. etrans. 1: apply maponpaths, id_left. apply pathsinv0, id_left. - intro c. use tpair. + use colimOfArrows. * intro b. induction b ; apply identity. * intros b1 b2 e. apply fromempty. exact e. + split ; cbn. * etrans. 1: apply postcompWithColimArrow. apply pathsinv0. use colimArrowUnique. intro b. etrans. 1: apply id_right. cbn. etrans. 2: apply assoc. etrans. 2: { apply maponpaths, pathsinv0. apply (colimArrowCommutes (BC (coproducts_diagram bool D (λ i : bool, (if i then F else G) c))) ). } induction b ; refine (_ @ ! id_left _) ; apply pathsinv0, id_left. * etrans. 1: apply postcompWithColimArrow. apply pathsinv0. use colimArrowUnique. intro b. etrans. 1: apply id_right. cbn. etrans. 2: apply assoc. etrans. 2: { apply maponpaths, pathsinv0. apply (colimArrowCommutes (BC (bincoproduct_diagram D (F c) (G c))) ). } induction b ; refine (_ @ ! id_left _) ; apply pathsinv0, id_left. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Sets. 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.Univalence. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering. 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.exponentials. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Monads.Monads. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Categories.HSET.Colimits. Require Import UniMath.CategoryTheory.Categories.HSET.Limits. Require Import UniMath.CategoryTheory.Categories.HSET.Structures. Require Import UniMath.CategoryTheory.Categories.HSET.Univalence. Require Import UniMath.CategoryTheory.Categories.StandardCategories. Require Import UniMath.CategoryTheory.Groupoids. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.FunctorCoalgebras. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Chains.Cochains. Require Import UniMath.CategoryTheory.Chains.CoAdamek. Require Import UniMath.CategoryTheory.Chains.OmegaContFunctors. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Actegories.Actegories. Require Import UniMath.CategoryTheory.Actegories.ConstructionOfActegories. Require Import UniMath.CategoryTheory.Actegories.MorphismsOfActegories. Require Import UniMath.CategoryTheory.Actegories.CoproductsInActegories. Require Import UniMath.CategoryTheory.Actegories.ConstructionOfActegoryMorphisms. Require Import UniMath.CategoryTheory.Monoidal.CategoriesOfMonoids. Require Import UniMath.CategoryTheory.Monoidal.Examples.MonoidalPointedObjects. Require Import UniMath.CategoryTheory.Monoidal.Examples.EndofunctorsMonoidalElementary. Require Import UniMath.CategoryTheory.Monoidal.Examples.MonadsAsMonoidsElementary. Require Import UniMath.SubstitutionSystems.EquivalenceLaxLineatorsHomogeneousCase. Require Import UniMath.SubstitutionSystems.MultiSortedBindingSig. Require Import UniMath.SubstitutionSystems.MultiSorted_alt. Require Import UniMath.SubstitutionSystems.MultiSorted_actegorical. Require Import UniMath.SubstitutionSystems.MultiSortedMonadConstruction_alt. Require Import UniMath.SubstitutionSystems.GeneralizedSubstitutionSystems. Require Import UniMath.SubstitutionSystems.ConstructionOfGHSS. Require Import UniMath.SubstitutionSystems.SigmaMonoids. Require Import UniMath.SubstitutionSystems.ContinuitySignature.ContinuityOfMultiSortedSigToFunctor. Require Import UniMath.SubstitutionSystems.ContinuitySignature.MultiSortedSignatureFunctorEquivalence. Require Import UniMath.SubstitutionSystems.ContinuitySignature.CommutingOfOmegaLimitsAndCoproducts. Require Import UniMath.SubstitutionSystems.ContinuitySignature.InstantiateHSET. Import BifunctorNotations. Import MonoidalNotations.