-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- `map₂` along equivalences of categories is an equivalence of categories.  -/
CategoryTheory.CostructuredArrow.map₂Iso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {T : D} →
          {S : CategoryTheory.Functor C D} →
            {A : Type u₃} →
              [inst_2 : CategoryTheory.Category.{v₃, u₃} A] →
                {B : Type u₄} →
                  [inst_3 : CategoryTheory.Category.{v₄, u₄} B] →
                    {U : CategoryTheory.Functor A B} →
                      {V : B} →
                        {F : C ≌ A} →
                          {G : D ≌ B} →
                            (α : F.functor.comp U ⟶ S.comp G.functor) →
                              (α' : F.inverse.comp S ⟶ U.comp G.inverse) →
                                CategoryTheory.CategoryStruct.comp S.leftUnitor.hom
                                      (CategoryTheory.CategoryStruct.comp S.rightUnitor.inv
                                        (CategoryTheory.CategoryStruct.comp (S.whiskerLeft G.unitIso.hom)
                                          (S.associator G.functor G.inverse).inv)) =
                                    CategoryTheory.CategoryStruct.comp
                                      (CategoryTheory.Functor.whiskerRight F.unitIso.hom S)
                                      (CategoryTheory.CategoryStruct.comp (F.functor.associator F.inverse S).hom
                                        (CategoryTheory.CategoryStruct.comp (F.functor.whiskerLeft α')
                                          (CategoryTheory.CategoryStruct.comp (F.functor.associator U G.inverse).inv
                                            (CategoryTheory.Functor.whiskerRight α G.inverse)))) →
                                  CategoryTheory.CategoryStruct.comp (F.inverse.whiskerLeft α)
                                        (CategoryTheory.CategoryStruct.comp (F.inverse.associator S G.functor).inv
                                          (CategoryTheory.CategoryStruct.comp
                                            (CategoryTheory.Functor.whiskerRight α' G.functor)
                                            (CategoryTheory.CategoryStruct.comp (U.associator G.inverse G.functor).hom
                                              (U.whiskerLeft G.counitIso.hom)))) =
                                      CategoryTheory.CategoryStruct.comp (F.inverse.associator F.functor U).inv
                                        (CategoryTheory.CategoryStruct.comp
                                          (CategoryTheory.Functor.whiskerRight F.counitIso.hom U)
                                          (CategoryTheory.CategoryStruct.comp U.leftUnitor.hom U.rightUnitor.inv)) →
                                    (β : G.functor.obj T ⟶ V) →
                                      (β' : G.inverse.obj V ⟶ T) →
                                        CategoryTheory.CategoryStruct.comp (G.inverse.map β) β' = G.unitIso.inv.app T →
                                          CategoryTheory.CategoryStruct.comp (G.functor.map β') β =
                                              G.counitIso.hom.app V →
                                            (CategoryTheory.CostructuredArrow S T ≌
                                              CategoryTheory.CostructuredArrow U V)