Definition make_algebra_simple (σ: signature_simple) (A: vec UU (pr1 σ)) (ops: (λ a, (el A)⋆ (dirprod_pr1 a) → el A (dirprod_pr2 a))⋆ (pr2 σ)) : algebra σ. Proof. exists (el A). unfold arity. induction σ as [ns ar]. simpl in A. revert ar ops. refine (list_ind _ _ _). - intros. cbn in nm. apply fromstn0. assumption. - simpl. intros x xs IHxs ops. induction ops as [op ops]. intro. cbn in nm. induction nm as [nm nmproof]. induction nm. + unfold star. exact op. + exact (IHxs ops (nm ,, nmproof)). Defined.
Require Import UniMath.Foundations.All.