proposition: Lemma hcomp_vcomp {a b c : C} (f1 g1 h1 : C ⟦ a, b ⟧) (f2 g2 h2 : C ⟦ b, c ⟧) (x1 : f1 ==> g1) (x2 : f2 ==> g2) (y1 : g1 ==> h1) (y2 : g2 ==> h2) : (x1 • y1) ⋆ (x2 • y2) = (x1 ⋆ x2) • (y1 ⋆ y2).
proof: Proof. unfold hcomp at 2 3. rewrite vassocr. rewrite vcomp_whisker. transitivity (((f1 ◃ x2) • ((x1 ▹ g2) • (y1 ▹ g2))) • (h1 ◃ y2)). 2: repeat rewrite vassocr; apply idpath. rewrite rwhisker_vcomp. rewrite <- vcomp_whisker. rewrite <- vassocr. rewrite lwhisker_vcomp. unfold hcomp. apply idpath. Qed.
imports: UniMath.Tactics.EnsureStructuredProofs UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.PrecategoryBinProduct