Definition make_algebra_simple_single_sorted (σ : signature_simple_single_sorted) (A : UU) (ops : (λ n: nat, vec A n → A)⋆ σ) : algebra σ. Proof. exists (λ _, A). unfold arity. revert σ ops. refine (list_ind _ _ _). - intros. cbn in nm. apply fromstn0. assumption. - intros x xs IHxs ops nm. simpl in ops. induction nm as [nm nmproof]. induction nm. + unfold star. exact (pr1 ops ∘ h1lower). + exact (IHxs (pr2 ops) (nm ,, nmproof)). Defined.
Require Import UniMath.Foundations.All.