{V : Type v} →
  [inst : CategoryTheory.Category.{w, v} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {C : Type u₁} →
        [CategoryTheory.EnrichedCategory V C] →
          {W : Type v'} →
            [inst_3 : CategoryTheory.Category.{w', v'} W] →
              [inst_4 : CategoryTheory.MonoidalCategory W] →
                (F : CategoryTheory.Functor V W) →
                  [inst_5 : F.LaxMonoidal] → CategoryTheory.EnrichedCategory W (CategoryTheory.TransportEnrichment F C)