∀ {B : Type u_3} [inst : CategoryTheory.Bicategory B] {a : B} (t : a ⟶ a) [inst_1 : CategoryTheory.Bicategory.Comonad t]
  {a_1 b c : CategoryTheory.LocallyDiscrete (CategoryTheory.Discrete Unit)} {f f' : a_1 ⟶ b} (η : f ⟶ f') (g : b ⟶ c),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id t) CategoryTheory.Bicategory.Comonad.comul =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Bicategory.Comonad.comul
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.CategoryStruct.id t) t)