∀ (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' →
                ∀ (hom : X ⟶ Y) (hom' : X' ⟶ Y'),
                  hom ≍ hom' →
                    ∀ (inv : Y ⟶ X) (inv' : Y' ⟶ X'),
                      inv ≍ inv' →
                        ∀ (hom_inv_id : CategoryTheory.CategoryStruct.comp hom inv = CategoryTheory.CategoryStruct.id X)
                          (hom_inv_id' :
                            CategoryTheory.CategoryStruct.comp hom' inv' = CategoryTheory.CategoryStruct.id X'),
                          hom_inv_id ≍ hom_inv_id' →
                            ∀
                              (inv_hom_id :
                                CategoryTheory.CategoryStruct.comp inv hom = CategoryTheory.CategoryStruct.id Y)
                              (inv_hom_id' :
                                CategoryTheory.CategoryStruct.comp inv' hom' = CategoryTheory.CategoryStruct.id Y'),
                              inv_hom_id ≍ inv_hom_id' →
                                { hom := hom, inv := inv, hom_inv_id := hom_inv_id, inv_hom_id := inv_hom_id } ≍
                                  { hom := hom', inv := inv', hom_inv_id := hom_inv_id', inv_hom_id := inv_hom_id' }