{D : Type u_1} →
  {D' : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} D] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D'] →
        {F : CategoryTheory.Functor D D'} →
          {C : Type u_3} →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
              [inst_3 : CategoryTheory.MonoidalCategory C] →
                [inst_4 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] →
                  [inst_5 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D'] →
                    {motive : F.RightLinear C → Sort u} →
                      (t : F.RightLinear C) →
                        ([toLaxRightLinear : F.LaxRightLinear C] →
                            [toOplaxRightLinear : F.OplaxRightLinear C] →
                              (μᵣ_comp_δᵣ :
                                  ∀ (d : D) (c : C),
                                    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxRightLinear.μᵣ F d c)
                                        (CategoryTheory.Functor.OplaxRightLinear.δᵣ F d c) =
                                      CategoryTheory.CategoryStruct.id
                                        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj (F.obj d)
                                          c)) →
                                (δᵣ_comp_μᵣ :
                                    ∀ (d : D) (c : C),
                                      CategoryTheory.CategoryStruct.comp
                                          (CategoryTheory.Functor.OplaxRightLinear.δᵣ F d c)
                                          (CategoryTheory.Functor.LaxRightLinear.μᵣ F d c) =
                                        CategoryTheory.CategoryStruct.id
                                          (F.obj
                                            (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d
                                              c))) →
                                  motive
                                    { toLaxRightLinear := toLaxRightLinear, toOplaxRightLinear := toOplaxRightLinear,
                                      μᵣ_comp_δᵣ := μᵣ_comp_δᵣ, δᵣ_comp_μᵣ := δᵣ_comp_μᵣ }) →
                          motive t