Definition SumMultiSortedSig : MultiSortedSig → MultiSortedSig → MultiSortedSig. Proof. intros s1 s2. use tpair. - apply (setcoprod (ops s1) (ops s2)). - induction 1 as [i|i]. + apply (arity s1 i). + apply (arity s2 i). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Combinatorics.Lists. Require Import UniMath.Combinatorics.StandardFiniteSets. 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.Categories.HSET.Core. Require Import UniMath.SubstitutionSystems.BindingSigToMonad. Section MultiSortedSigFromBindingSig. Definition arFromBindingSig : I → list (list sort × sort) × sort. Definition MultiSortedSigFromBindingSig : MultiSortedSig := I ,, arFromBindingSig. End MultiSortedSigFromBindingSig.