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