∀ {𝒮 : Type u_4} [inst : CategoryTheory.Category.{u_3, u_4} 𝒮] {a b c d e : CategoryTheory.BasedCategory 𝒮}
  (f : CategoryTheory.BasedFunctor a b) (g : CategoryTheory.BasedFunctor b c) (h : CategoryTheory.BasedFunctor c d)
  (i : CategoryTheory.BasedFunctor d e),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.BasedCategory.whiskerRight (CategoryTheory.BasedNatIso.id ((f.comp g).comp h)).hom i)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.BasedNatIso.id ((f.comp (g.comp h)).comp i)).hom
        (CategoryTheory.BasedCategory.whiskerLeft f (CategoryTheory.BasedNatIso.id ((g.comp h).comp i)).hom)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.BasedNatIso.id (((f.comp g).comp h).comp i)).hom
      (CategoryTheory.BasedNatIso.id ((f.comp g).comp (h.comp i))).hom