Definition make_algebra_simple_single_sorted' (σ : signature_simple_single_sorted) (A : hSet) (ops : (λ n: nat, iterfun (vec_fill (pr1hSet A) n) A)⋆ σ) : algebra σ. Proof. refine (make_algebra_simple_single_sorted σ A _). refine (h1map _ ops). intro a. induction (@hvec_vec_fill A a). exact uncurrify. Defined.
Require Import UniMath.Foundations.All.