∀ {B : Type u_2} {C : Type u_4} [inst : CategoryTheory.Category.{u_1, u_2} B]
  [inst_1 : CategoryTheory.Category.{u_3, u_4} C] {U : CategoryTheory.Functor B C} {F : CategoryTheory.Functor C B}
  (adj₁ : F ⊣ U) (X : B),
  CategoryTheory.CategoryStruct.comp (F.map (U.map (adj₁.counit.app X))) (adj₁.counit.app X) =
    CategoryTheory.CategoryStruct.comp (adj₁.counit.app (F.obj (U.obj X))) (adj₁.counit.app X)