{B : Type u} →
  {inst : CategoryTheory.Bicategory B} →
    {a b : B} →
      {f : a ⟶ b} →
        {g : b ⟶ a} →
          {P : Sort u_1} →
            {unit : CategoryTheory.CategoryStruct.id a ⟶ CategoryTheory.CategoryStruct.comp f g} →
              {counit : CategoryTheory.CategoryStruct.comp g f ⟶ CategoryTheory.CategoryStruct.id b} →
                {left_triangle :
                    autoParam
                      (CategoryTheory.Bicategory.leftZigzag unit counit =
                        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor f).hom
                          (CategoryTheory.Bicategory.rightUnitor f).inv)
                      CategoryTheory.Bicategory.Adjunction.left_triangle._autoParam} →
                  {right_triangle :
                      autoParam
                        (CategoryTheory.Bicategory.rightZigzag unit counit =
                          CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor g).hom
                            (CategoryTheory.Bicategory.leftUnitor g).inv)
                        CategoryTheory.Bicategory.Adjunction.right_triangle._autoParam} →
                    {unit' : CategoryTheory.CategoryStruct.id a ⟶ CategoryTheory.CategoryStruct.comp f g} →
                      {counit' : CategoryTheory.CategoryStruct.comp g f ⟶ CategoryTheory.CategoryStruct.id b} →
                        {left_triangle' :
                            autoParam
                              (CategoryTheory.Bicategory.leftZigzag unit' counit' =
                                CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor f).hom
                                  (CategoryTheory.Bicategory.rightUnitor f).inv)
                              CategoryTheory.Bicategory.Adjunction.left_triangle._autoParam} →
                          {right_triangle' :
                              autoParam
                                (CategoryTheory.Bicategory.rightZigzag unit' counit' =
                                  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor g).hom
                                    (CategoryTheory.Bicategory.leftUnitor g).inv)
                                CategoryTheory.Bicategory.Adjunction.right_triangle._autoParam} →
                            { unit := unit, counit := counit, left_triangle := left_triangle,
                                  right_triangle := right_triangle } =
                                { unit := unit', counit := counit', left_triangle := left_triangle',
                                  right_triangle := right_triangle' } →
                              (unit ≍ unit' → counit ≍ counit' → P) → P