∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a : B} (t : a ⟶ a) [inst_1 : CategoryTheory.Bicategory.Comonad t],
  CategoryTheory.CategoryStruct.comp CategoryTheory.Bicategory.Comonad.comul
      (CategoryTheory.Bicategory.whiskerRight CategoryTheory.Bicategory.Comonad.counit t) =
    (CategoryTheory.Bicategory.leftUnitor t).inv