proposition: Lemma path_precomp_var_term_algebra_to_hom_term_algebra : forall (f : TermAlgebra C $-> A), hom_term_algebra A (precomp_var_term_algebra f) = f.
proof: Proof. intro f. apply path_homomorphism. funext s T. induction T as [|u c h]. - reflexivity. - refine (_ @ (is_homomorphism f u c)^). refine (ap u.#A _). funext i. apply h. Defined.
imports: HoTT.Algebra.Universal.Algebra HoTT.HSet HoTT.Classes.interfaces.canonical_names HoTT.Algebra.Universal.Homomorphism HoTT.Algebra.Universal.Congruence