{C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            (F : CategoryTheory.Functor C D) →
              [inst_4 : F.Monoidal] →
                [F.Faithful] →
                  {X Y : C} →
                    (eval :
                        CategoryTheory.MonoidalCategoryStruct.tensorObj Y X ⟶
                          CategoryTheory.MonoidalCategoryStruct.tensorUnit C) →
                      (coeval :
                          CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶
                            CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) →
                        [inst_6 : CategoryTheory.ExactPairing (F.obj X) (F.obj Y)] →
                          F.map eval =
                              CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ F Y X)
                                (CategoryTheory.CategoryStruct.comp (ε_ (F.obj X) (F.obj Y))
                                  (CategoryTheory.Functor.LaxMonoidal.ε F)) →
                            F.map coeval =
                                CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.η F)
                                  (CategoryTheory.CategoryStruct.comp (η_ (F.obj X) (F.obj Y))
                                    (CategoryTheory.Functor.LaxMonoidal.μ F X Y)) →
                              CategoryTheory.ExactPairing X Y