∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_4, u_1} C] {D : Type u_3}
  [inst_1 : CategoryTheory.Category.{u_2, u_3} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C}
  (h : L ⊣ R),
  CategoryTheory.CategoryStruct.comp
      {
        app := fun x =>
          CategoryTheory.CategoryStruct.id (((CategoryTheory.Comonad.comparison h).comp h.toComonad.forget).obj x),
        naturality := ⋯ }
      { app := fun x => CategoryTheory.CategoryStruct.id (L.obj x), naturality := ⋯ } =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.Comonad.comparison h).comp h.toComonad.forget)