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