∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] (X : C),
  { app := fun x g => CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.id X), naturality := ⋯ } =
    CategoryTheory.CategoryStruct.id
      { obj := fun Y => Opposite.unop Y ⟶ X, map := fun {X_1 Y} f g => CategoryTheory.CategoryStruct.comp f.unop g,
        map_id := ⋯, map_comp := ⋯ }