{C D : CategoryTheory.Cat} →
  (e : ↑C ≌ ↑D) →
    (h₁ : ∀ (X : ↑C), e.inverse.obj (e.functor.obj X) = X) →
      (h₂ : ∀ (Y : ↑D), e.functor.obj (e.inverse.obj Y) = Y) →
        autoParam (∀ (X : ↑C), e.unitIso.hom.app X = CategoryTheory.eqToHom ⋯) CategoryTheory.Cat.isoOfEquiv._auto_1 →
          autoParam (∀ (Y : ↑D), e.counitIso.hom.app Y = CategoryTheory.eqToHom ⋯)
              CategoryTheory.Cat.isoOfEquiv._auto_3 →
            (C ≅ D)