{J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} C] →
        (X : C) → (CategoryTheory.Functor.const Jᵒᵖ).obj (Opposite.op X) ≅ ((CategoryTheory.Functor.const J).obj X).op