proposition: Lemma assoc_homomorphism_compose `{Funext} {σ} {A B C D : Algebra σ} (h : C $-> D) (g : B $-> C) (f : A $-> B) : (h $o g) $o f = h $o (g $o f).
proof: Proof. by apply path_homomorphism. Defined.
imports: HoTT.Algebra.Universal.Algebra HoTT.WildCat.Core HoTT.Types