proposition: Theorem ump_term_algebra : (TermAlgebra C $-> A) <~> (forall s, C s -> A s).
proof: Proof. exact (Build_Equiv _ _ precomp_var_term_algebra _). Defined.
imports: HoTT.Algebra.Universal.Algebra HoTT.HSet HoTT.Classes.interfaces.canonical_names HoTT.Algebra.Universal.Homomorphism HoTT.Algebra.Universal.Congruence