{P : Sort u} →
  {C : Type u₁} →
    {inst : CategoryTheory.Category.{v₁, u₁} C} →
      {D : Type u₂} →
        {inst_1 : CategoryTheory.Category.{v₂, u₂} D} →
          {F : CategoryTheory.Functor C D} →
            {G : CategoryTheory.Functor D C} →
              {t : F ⊣ G} →
                {C' : Type u₁} →
                  {inst' : CategoryTheory.Category.{v₁, u₁} C'} →
                    {D' : Type u₂} →
                      {inst'_1 : CategoryTheory.Category.{v₂, u₂} D'} →
                        {F' : CategoryTheory.Functor C' D'} →
                          {G' : CategoryTheory.Functor D' C'} →
                            {t' : F' ⊣ G'} →
                              C = C' →
                                inst ≍ inst' →
                                  D = D' →
                                    inst_1 ≍ inst'_1 →
                                      F ≍ F' → G ≍ G' → t ≍ t' → CategoryTheory.Adjunction.noConfusionType P t t'