Definition vsignature (σ : signature) (V: varspec σ): signature := make_signature (sorts σ) (setcoprod (names σ) V) (sumofmaps (ar σ) (λ v, nil ,, varsort v)).
Require Import UniMath.Foundations.All. Require Import UniMath.Algebra.Universal.SortedTypes.