∀ {V : Type u_5} [inst : CategoryTheory.Category.{u_4, u_5} V] [inst_1 : CategoryTheory.MonoidalCategory V]
  (C : Type u_3) [inst_2 : CategoryTheory.Category.{u_6, u_3} C] [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V C]
  {W : Type u_2} [inst_4 : CategoryTheory.Category.{u_1, u_2} W] [inst_5 : CategoryTheory.MonoidalCategory W]
  (F : CategoryTheory.Functor V W) [inst_6 : F.LaxMonoidal]
  (e :
    (v : V) →
      (CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ v) ≃
        (CategoryTheory.MonoidalCategoryStruct.tensorUnit W ⟶ F.obj v)),
  (∀ (v : V) (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ v),
      (e v) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F) (F.map f)) →
    ∀ {X Y Z : CategoryTheory.TransportEnrichment F C} (f : X ⟶ Y) (g : Y ⟶ Z),
      ((CategoryTheory.eHomEquiv V).trans (e (X ⟶[V] Z))) (CategoryTheory.CategoryStruct.comp f g) =
        CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit W)).inv
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.MonoidalCategoryStruct.tensorHom (((CategoryTheory.eHomEquiv V).trans (e (X ⟶[V] Y))) f)
              (((CategoryTheory.eHomEquiv V).trans (e (Y ⟶[V] Z))) g))
            (CategoryTheory.eComp W X Y Z))