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