Definition make_algebra' {σ: signature} (A : sUU (sorts σ)) (ops: ∏ nm: names σ, iterfun (vec_map A (arity nm)) (A (sort nm))) : algebra σ := A ,, λ nm, uncurrify (ops nm).
Require Import UniMath.Foundations.All.