proposition: Lemma CCS_Functor_Initial : Initial (FunctorAlg CCS_Functor).
proof: Proof. apply SignatureInitialAlgebraSetSort. apply is_omega_cocont_MultiSortedSigToSignature. apply slice_precat_colims_of_shape, ColimsHSET_of_shape. Defined.
imports: UniMath.Foundations.PartD UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Lists UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.Colimits UniMath.CategoryTheory.Categories.HSET.Limits UniMath.CategoryTheory.Categories.HSET.Slice UniMath.CategoryTheory.Chains.Chains UniMath.CategoryTheory.Chains.OmegaCocontFunctors UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Initial UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Products UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.FunctorAlgebras UniMath.CategoryTheory.exponentials UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Monads.Monads UniMath.CategoryTheory.slicecat UniMath.SubstitutionSystems.Signatures UniMath.SubstitutionSystems.SumOfSignatures UniMath.SubstitutionSystems.BinProductOfSignatures UniMath.SubstitutionSystems.SubstitutionSystems UniMath.SubstitutionSystems.LiftingInitial_alt UniMath.SubstitutionSystems.MonadsFromSubstitutionSystems UniMath.SubstitutionSystems.Notation UniMath.SubstitutionSystems.SignatureExamples UniMath.SubstitutionSystems.BindingSigToMonad UniMath.SubstitutionSystems.MonadsMultiSorted UniMath.SubstitutionSystems.MultiSorted UniMath.SubstitutionSystems.MultiSortedMonadConstruction