{C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D₁ : Type u_3} →
      {D₂ : Type u_4} →
        {E : Type u_5} →
          {inst : CategoryTheory.Category.{v_1, u_1} C₁} →
            {inst_1 : CategoryTheory.Category.{v_2, u_2} C₂} →
              {inst_2 : CategoryTheory.Category.{v_3, u_3} D₁} →
                {inst_3 : CategoryTheory.Category.{v_4, u_4} D₂} →
                  {inst_4 : CategoryTheory.Category.{v_5, u_5} E} →
                    {L₁ : CategoryTheory.Functor C₁ D₁} →
                      {L₂ : CategoryTheory.Functor C₂ D₂} →
                        {W₁ : CategoryTheory.MorphismProperty C₁} →
                          {W₂ : CategoryTheory.MorphismProperty C₂} →
                            {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ E)} →
                              {F' : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ E)} →
                                {P : Sort u} →
                                  {iso iso' : (((CategoryTheory.Functor.whiskeringLeft₂ E).obj L₁).obj L₂).obj F' ≅ F} →
                                    { iso := iso } = { iso := iso' } → (iso ≍ iso' → P) → P