Definition fromterm {A: sUU (sorts σ)} {V: varspec σ} (op : (∏ nm : names σ, A⋆ (arity nm) → A (sort nm))) (α : assignment A V) : term σ V s→ A. Proof. refine (@fromgterm (vsignature σ V) A _). induction nm as [nm | v]. - exact (op nm). - exact (λ _, α v). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.Algebra.Universal.SortedTypes.