{C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
            {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)} →
              {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} →
                (adj : (X₁ : C₁) → F.obj X₁ ⊣ G.obj (Opposite.op X₁)) →
                  autoParam
                      (∀ {X₁ Y₁ : C₁} (f : X₁ ⟶ Y₁) {X₂ : C₂} {X₃ : C₃} (g : (F.obj Y₁).obj X₂ ⟶ X₃),
                        ((adj X₁).homEquiv X₂ X₃) (CategoryTheory.CategoryStruct.comp ((F.map f).app X₂) g) =
                          CategoryTheory.CategoryStruct.comp (((adj Y₁).homEquiv X₂ X₃) g) ((G.map f.op).app X₃))
                      CategoryTheory.ParametrizedAdjunction.mk'._auto_1 →
                    (F ⊣₂ G)