Definition SigmaMonoidOfMultiSortedSig_CAT (sig : MultiSortedSig sort) : SigmaMonoid (MultiSortedSigToStrength' sig). Proof. apply mhss_to_sigma_monoid. exact (MHSSOfMultiSortedSig_CAT sig). 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.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.FunctorAlgebras. Require Import UniMath.CategoryTheory.exponentials. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Chains.All. 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.StandardCategories. Require Import UniMath.CategoryTheory.Groupoids. Require Import UniMath.SubstitutionSystems.Signatures. Require Import UniMath.SubstitutionSystems.SumOfSignatures. Require Import UniMath.SubstitutionSystems.BinProductOfSignatures. Require Import UniMath.SubstitutionSystems.SignatureExamples. 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.Bicategories.PseudoFunctors.Examples.CurryingInBicatOfCats. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.Equivalences.CompositesAndInverses. Require Import UniMath.Bicategories.PseudoFunctors.Biadjunction. Require Import UniMath.CategoryTheory.Categories.HSET.Univalence. Import BifunctorNotations. Import MonoidalNotations. use (SigmaMonoidFromInitialAlgebraInitial (MultiSortedSigToStrength' sig) BCsortToC2). assert (Hyp := SigmaMonoid_is_compatible (MultiSortedSigToStrengthFromSelfCAT sig) σ).