fact: Definition make_algebra_simple (σ: signature_simple) (A: vec UU (pr1 σ)) (ops: (λ a, (el A)⋆ (dirprod_pr1 a) → el A (dirprod_pr2 a))⋆ (pr2 σ)) : algebra σ.
imports: UniMath.Foundations.All UniMath.Algebra.Universal.SortedTypes UniMath.Algebra.Universal.Signatures