∀ (C C' : Type u),
  C = C' →
    ∀ (inst : CategoryTheory.Category.{v, u} C) (inst' : CategoryTheory.Category.{v, u} C'),
      inst ≍ inst' →
        ∀ (X : C) (X' : C'),
          X ≍ X' → ∀ (Y : C) (Y' : C'), Y ≍ Y' → ∀ (self : X ≅ Y) (self' : X' ≅ Y'), self ≍ self' → self.inv ≍ self'.inv