no goals
C : Type u
inst✝ : Category C
F : C ⥤ C
A A₀ A₁ A₂ : Algebra F
f : A₀ ⟶ A₁
g : A₁ ⟶ A₂
h : Limits.IsInitial A
⊢ F.map (strInv h ≫ A.str) ≫ A.str = A.str ≫ strInv h ≫ A.str
rw [←Category.assoc, F.map_comp, strInv, ←Hom.h]