∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] (F : CategoryTheory.Functor C (Type (max u_3 u_1 u_2)))
  {X Y : CategoryTheory.Functor C (Type (max u_3 u_1 u_2))} (f : X ⟶ Y) ⦃X_1 Y_1 : C⦄ (f_1 : X_1 ⟶ Y_1),
  CategoryTheory.CategoryStruct.comp ((F.functorHom X).map f_1) (CategoryTheory.FunctorToTypes.rightAdj_map f Y_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.FunctorToTypes.rightAdj_map f X_1) ((F.functorHom Y).map f_1)