Definition make_signature (S: decSet) (O: hSet) (ar: O → list S × S) : signature := S ,, (O ,, ar).
Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Combinatorics.MoreLists.