∀ {J : Type u_1} [inst : CategoryTheory.Category.{u_4, u_1} J] {C : Type u_3}
  [inst_1 : CategoryTheory.Category.{u_2, u_3} C] (X : C),
  CategoryTheory.CategoryStruct.comp
      { app := fun x => CategoryTheory.CategoryStruct.id (((CategoryTheory.Functor.const J).obj X).op.obj x),
        naturality := ⋯ }
      {
        app := fun x =>
          CategoryTheory.CategoryStruct.id (((CategoryTheory.Functor.const Jᵒᵖ).obj (Opposite.op X)).obj x),
        naturality := ⋯ } =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.const J).obj X).op