Definition arity {σ: signature} (nm: names σ) : list (sorts σ) := pr1 (ar σ nm).
Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Combinatorics.MoreLists.