Library UniMath.SubstitutionSystems.All

Require Export UniMath.SubstitutionSystems.Notation.
Require Export UniMath.SubstitutionSystems.Signatures.
Require Export UniMath.SubstitutionSystems.BinSumOfSignatures.
Require Export UniMath.SubstitutionSystems.SumOfSignatures.
Require Export UniMath.SubstitutionSystems.BinProductOfSignatures.
Require Export UniMath.SubstitutionSystems.SubstitutionSystems.
Require Export UniMath.SubstitutionSystems.SimplifiedHSS.SubstitutionSystems.
Require Export UniMath.SubstitutionSystems.SignaturesEquivRelativeStrength.
Require Export UniMath.SubstitutionSystems.GeneralizedSubstitutionSystems.
Require Export UniMath.SubstitutionSystems.MonadsFromSubstitutionSystems.
Require Export UniMath.SubstitutionSystems.SimplifiedHSS.MonadsFromSubstitutionSystems.
Require Export UniMath.SubstitutionSystems.GenMendlerIteration.
Require Export UniMath.SubstitutionSystems.GenMendlerIteration_alt.
Require Export UniMath.SubstitutionSystems.ActionScenarioForGenMendlerIteration_alt.
Require Export UniMath.SubstitutionSystems.ApplicationsGenMendlerIteration_alt.
Require Export UniMath.SubstitutionSystems.LiftingInitial.
Require Export UniMath.SubstitutionSystems.SimplifiedHSS.LiftingInitial.
Require Export UniMath.SubstitutionSystems.LiftingInitial_alt.
Require Export UniMath.SubstitutionSystems.SimplifiedHSS.LiftingInitial_alt.
Require Export UniMath.SubstitutionSystems.ModulesFromSignatures.
Require Export UniMath.SubstitutionSystems.SimplifiedHSS.ModulesFromSignatures.
Require Export UniMath.SubstitutionSystems.LamSignature.
Require Export UniMath.SubstitutionSystems.Lam.
Require Export UniMath.SubstitutionSystems.SimplifiedHSS.Lam.
Require Export UniMath.SubstitutionSystems.SignatureExamples.
Require Export UniMath.SubstitutionSystems.SignatureCategory.
Require Export UniMath.SubstitutionSystems.SubstitutionSystems_Summary.
Require Export UniMath.SubstitutionSystems.SimplifiedHSS.SubstitutionSystems_Summary.
Require Export UniMath.SubstitutionSystems.LamHSET.
Require Export UniMath.SubstitutionSystems.SimplifiedHSS.LamHSET.
Require Export UniMath.SubstitutionSystems.BindingSigToMonad.
Require Export UniMath.SubstitutionSystems.SimplifiedHSS.BindingSigToMonad.
Require Export UniMath.SubstitutionSystems.LamFromBindingSig.
Require Export UniMath.SubstitutionSystems.SimplifiedHSS.LamFromBindingSig.
Require Export UniMath.SubstitutionSystems.MLTT79.
Require Export UniMath.SubstitutionSystems.SimplifiedHSS.MLTT79.
Require Export UniMath.SubstitutionSystems.FromBindingSigsToMonads_Summary.
Require Export UniMath.SubstitutionSystems.SimplifiedHSS.FromBindingSigsToMonads_Summary.
Require Export UniMath.SubstitutionSystems.SortIndexing.
Require Export UniMath.SubstitutionSystems.MonadsMultiSorted.
Require Export UniMath.SubstitutionSystems.MonadsMultiSorted_alt.
Require Export UniMath.SubstitutionSystems.MultiSortedBindingSig.
Require Export UniMath.SubstitutionSystems.MultiSorted.
Require Export UniMath.SubstitutionSystems.MultiSortedMonadConstruction.
Require Export UniMath.SubstitutionSystems.SimplifiedHSS.MultiSortedMonadConstruction.
Require Export UniMath.SubstitutionSystems.MultiSorted_alt.
Require Export UniMath.SubstitutionSystems.MultiSortedMonadConstruction_alt.
Require Export UniMath.SubstitutionSystems.SimplifiedHSS.MultiSortedMonadConstruction_alt.
Require Export UniMath.SubstitutionSystems.MonadicSubstitution_alt.
Require Export UniMath.SubstitutionSystems.SimplifiedHSS.MonadicSubstitution_alt.
Require Export UniMath.SubstitutionSystems.STLC.
Require Export UniMath.SubstitutionSystems.SimplifiedHSS.STLC.
Require Export UniMath.SubstitutionSystems.STLC_alt.
Require Export UniMath.SubstitutionSystems.SimplifiedHSS.STLC_alt.
Require Export UniMath.SubstitutionSystems.CCS.
Require Export UniMath.SubstitutionSystems.SimplifiedHSS.CCS.
Require Export UniMath.SubstitutionSystems.CCS_alt.
Require Export UniMath.SubstitutionSystems.SimplifiedHSS.CCS_alt.
Require Export UniMath.SubstitutionSystems.PCF_alt.
Require Export UniMath.SubstitutionSystems.SimplifiedHSS.PCF_alt.
Require Export UniMath.SubstitutionSystems.ActionBasedStrengthOnHomsInBicat.
Require Export UniMath.SubstitutionSystems.EquivalenceSignaturesWithActegoryMorphisms.
Require Export UniMath.SubstitutionSystems.EquivalenceLaxLineatorsHomogeneousCase.
Require Export UniMath.SubstitutionSystems.SigmaMonoids.
Require Export UniMath.SubstitutionSystems.ConstructionOfGHSS.
Require Export UniMath.SubstitutionSystems.BindingSigToMonad_actegorical.
Require Export UniMath.SubstitutionSystems.ContinuitySignature.GeneralLemmas.
Require Export UniMath.SubstitutionSystems.ContinuitySignature.CommutingOfOmegaLimitsAndCoproducts.
Require Export UniMath.SubstitutionSystems.ContinuitySignature.ContinuityOfMultiSortedSigToFunctor.
Require Export UniMath.SubstitutionSystems.ContinuitySignature.MultiSortedSignatureFunctorEquivalence.
Require Export UniMath.SubstitutionSystems.ContinuitySignature.InstantiateHSET.
Require Export UniMath.SubstitutionSystems.MultiSorted_actegorical.
Require Export UniMath.SubstitutionSystems.MultiSortedMonadConstruction_actegorical.
Require Export UniMath.SubstitutionSystems.MultiSortedMonadConstruction_coind_actegorical.
Require Export UniMath.SubstitutionSystems.MultiSortedEmbeddingIndCoindHSET.
Require Export UniMath.SubstitutionSystems.UntypedForests.
Require Export UniMath.SubstitutionSystems.Forests.
Require Export UniMath.SubstitutionSystems.STLC_actegorical.
Require Export UniMath.SubstitutionSystems.STLC_actegorical_abstractcat.