∀ {C : Type u₁} {D : Type u₂} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {functor : CategoryTheory.Functor C D} {inverse : CategoryTheory.Functor D C}
  {unitIso : CategoryTheory.Functor.id C ≅ functor.comp inverse}
  {counitIso : inverse.comp functor ≅ CategoryTheory.Functor.id D}
  {functor_unitIso_comp :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (functor.map (unitIso.hom.app X)) (counitIso.hom.app (functor.obj X)) =
          CategoryTheory.CategoryStruct.id (functor.obj X))
      CategoryTheory.Equivalence.functor_unitIso_comp._autoParam}
  {functor_1 : CategoryTheory.Functor C D} {inverse_1 : CategoryTheory.Functor D C}
  {unitIso_1 : CategoryTheory.Functor.id C ≅ functor_1.comp inverse_1}
  {counitIso_1 : inverse_1.comp functor_1 ≅ CategoryTheory.Functor.id D}
  {functor_unitIso_comp_1 :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (functor_1.map (unitIso_1.hom.app X))
            (counitIso_1.hom.app (functor_1.obj X)) =
          CategoryTheory.CategoryStruct.id (functor_1.obj X))
      CategoryTheory.Equivalence.functor_unitIso_comp._autoParam},
  { functor := functor, inverse := inverse, unitIso := unitIso, counitIso := counitIso,
        functor_unitIso_comp := functor_unitIso_comp } =
      { functor := functor_1, inverse := inverse_1, unitIso := unitIso_1, counitIso := counitIso_1,
        functor_unitIso_comp := functor_unitIso_comp_1 } →
    functor = functor_1 ∧ inverse = inverse_1 ∧ unitIso ≍ unitIso_1 ∧ counitIso ≍ counitIso_1