Definition make_algebra_simple' (σ: signature_simple) (A: vec UU (pr1 σ)) (ops: (λ a, iterfun (vec_map (el A) (pr2 (dirprod_pr1 a))) (el A (dirprod_pr2 a)))⋆ (pr2 σ)) : algebra σ := make_algebra_simple σ A (h1map (λ _, uncurrify) ops).
Require Import UniMath.Foundations.All.