Definition make_signature_single_sorted (O: hSet) (ar: O → nat) : signature := make_signature (unit,, isdecequnit) O (λ op, fill tt (ar op) ,, tt).
Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Combinatorics.MoreLists.