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. 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.PrecategoryBinProduct.