{B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    (F : CategoryTheory.OplaxFunctor (CategoryTheory.LocallyDiscrete (CategoryTheory.Discrete Unit)) B) →
      CategoryTheory.Bicategory.Comonad (F.map (CategoryTheory.CategoryStruct.id { as := { as := () } }))