proposition: Lemma path_hom_term_algebra_to_precomp_var_term_algebra : forall (f : forall s, C s -> A s), precomp_var_term_algebra (hom_term_algebra A f) = f.
proof: Proof. intro f. by funext s a. Defined.
imports: HoTT.Algebra.Universal.Algebra HoTT.HSet HoTT.Classes.interfaces.canonical_names HoTT.Algebra.Universal.Homomorphism HoTT.Algebra.Universal.Congruence