{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] →
          {motive : CategoryTheory.MonoidalCategory.MonoidalRightAction C D → Sort u} →
            ([toMonoidalRightActionStruct : CategoryTheory.MonoidalCategory.MonoidalRightActionStruct C D] →
                (actionHom_def :
                    ∀ {c c' : C} {d d' : D} (f : d ⟶ d') (g : c ⟶ c'),
                      CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom f g =
                        CategoryTheory.CategoryStruct.comp
                          (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f c)
                          (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight d' g)) →
                  (actionHomRight_id :
                      ∀ (c : C) (d : D),
                        CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight d
                            (CategoryTheory.CategoryStruct.id c) =
                          CategoryTheory.CategoryStruct.id
                            (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d c)) →
                    (id_actionHomLeft :
                        ∀ (c : C) (d : D),
                          CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft
                              (CategoryTheory.CategoryStruct.id d) c =
                            CategoryTheory.CategoryStruct.id
                              (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d c)) →
                      (actionHom_comp :
                          ∀ {c c' c'' : C} {d d' d'' : D} (f₁ : d ⟶ d') (f₂ : d' ⟶ d'') (g₁ : c ⟶ c') (g₂ : c' ⟶ c''),
                            CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom
                                (CategoryTheory.CategoryStruct.comp f₁ f₂) (CategoryTheory.CategoryStruct.comp g₁ g₂) =
                              CategoryTheory.CategoryStruct.comp
                                (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom f₁ g₁)
                                (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom f₂ g₂)) →
                        (actionAssocIso_hom_naturality :
                            ∀ {d₁ d₂ : D} {c₁ c₂ c₃ c₄ : C} (f : d₁ ⟶ d₂) (g : c₁ ⟶ c₂) (h : c₃ ⟶ c₄),
                              CategoryTheory.CategoryStruct.comp
                                  (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom f
                                    (CategoryTheory.MonoidalCategoryStruct.tensorHom g h))
                                  (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d₂ c₂
                                      c₄).hom =
                                CategoryTheory.CategoryStruct.comp
                                  (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d₁ c₁
                                      c₃).hom
                                  (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom
                                    (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom f g) h)) →
                          (actionUnitIso_hom_naturality :
                              ∀ {d d' : D} (f : d ⟶ d'),
                                CategoryTheory.CategoryStruct.comp
                                    (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso d).hom f =
                                  CategoryTheory.CategoryStruct.comp
                                    (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f
                                      (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
                                    (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso d').hom) →
                            (actionHomRight_whiskerRight :
                                ∀ {c' c'' : C} (f : c' ⟶ c'') (c : C) (d : D),
                                  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight d
                                      (CategoryTheory.MonoidalCategoryStruct.whiskerRight f c) =
                                    CategoryTheory.CategoryStruct.comp
                                      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d c'
                                          c).hom
                                      (CategoryTheory.CategoryStruct.comp
                                        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft
                                          (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight d f)
                                          c)
                                        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d c''
                                            c).inv)) →
                              (whiskerRight_actionHomLeft :
                                  ∀ (c : C) {c' c'' : C} (f : c' ⟶ c'') (d : D),
                                    CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight d
                                        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft c f) =
                                      CategoryTheory.CategoryStruct.comp
                                        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d c
                                            c').hom
                                        (CategoryTheory.CategoryStruct.comp
                                          (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight
                                            (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d c) f)
                                          (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d c
                                              c'').inv)) →
                                (actionHom_associator :
                                    ∀ (c₁ c₂ c₃ : C) (d : D),
                                      CategoryTheory.CategoryStruct.comp
                                          (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight d
                                            (CategoryTheory.MonoidalCategoryStruct.associator c₁ c₂ c₃).hom)
                                          (CategoryTheory.CategoryStruct.comp
                                            (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d
                                                c₁ (CategoryTheory.MonoidalCategoryStruct.tensorObj c₂ c₃)).hom
                                            (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso
                                                (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d
                                                  c₁)
                                                c₂ c₃).hom) =
                                        CategoryTheory.CategoryStruct.comp
                                          (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d
                                              (CategoryTheory.MonoidalCategoryStruct.tensorObj c₁ c₂) c₃).hom
                                          (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft
                                            (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d
                                                c₁ c₂).hom
                                            c₃)) →
                                  (actionHom_leftUnitor :
                                      ∀ (c : C) (d : D),
                                        CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight d
                                            (CategoryTheory.MonoidalCategoryStruct.leftUnitor c).hom =
                                          CategoryTheory.CategoryStruct.comp
                                            (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d
                                                (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) c).hom
                                            (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft
                                              (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso
                                                  d).hom
                                              c)) →
                                    (actionHom_rightUnitor :
                                        ∀ (c : C) (d : D),
                                          CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight d
                                              (CategoryTheory.MonoidalCategoryStruct.rightUnitor c).hom =
                                            CategoryTheory.CategoryStruct.comp
                                              (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso
                                                  d c (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom
                                              (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso
                                                  (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d
                                                    c)).hom) →
                                      motive
                                        { toMonoidalRightActionStruct := toMonoidalRightActionStruct,
                                          actionHom_def := actionHom_def, actionHomRight_id := actionHomRight_id,
                                          id_actionHomLeft := id_actionHomLeft, actionHom_comp := actionHom_comp,
                                          actionAssocIso_hom_naturality := actionAssocIso_hom_naturality,
                                          actionUnitIso_hom_naturality := actionUnitIso_hom_naturality,
                                          actionHomRight_whiskerRight := actionHomRight_whiskerRight,
                                          whiskerRight_actionHomLeft := whiskerRight_actionHomLeft,
                                          actionHom_associator := actionHom_associator,
                                          actionHom_leftUnitor := actionHom_leftUnitor,
                                          actionHom_rightUnitor := actionHom_rightUnitor }) →
              (t : CategoryTheory.MonoidalCategory.MonoidalRightAction C D) → motive t