{m : Type → Type} →
  {motive : Mathlib.Tactic.BicategoryLike.MonadMor₂Iso m → Sort u} →
    ((associatorM :
          Mathlib.Tactic.BicategoryLike.Mor₁ →
            Mathlib.Tactic.BicategoryLike.Mor₁ →
              Mathlib.Tactic.BicategoryLike.Mor₁ → m Mathlib.Tactic.BicategoryLike.StructuralAtom) →
        (leftUnitorM rightUnitorM id₂M :
            Mathlib.Tactic.BicategoryLike.Mor₁ → m Mathlib.Tactic.BicategoryLike.StructuralAtom) →
          (coherenceHomM :
              Mathlib.Tactic.BicategoryLike.Mor₁ →
                Mathlib.Tactic.BicategoryLike.Mor₁ → Lean.Expr → m Mathlib.Tactic.BicategoryLike.CoherenceHom) →
            (comp₂M :
                Mathlib.Tactic.BicategoryLike.Mor₂Iso →
                  Mathlib.Tactic.BicategoryLike.Mor₂Iso → m Mathlib.Tactic.BicategoryLike.Mor₂Iso) →
              (whiskerLeftM :
                  Mathlib.Tactic.BicategoryLike.Mor₁ →
                    Mathlib.Tactic.BicategoryLike.Mor₂Iso → m Mathlib.Tactic.BicategoryLike.Mor₂Iso) →
                (whiskerRightM :
                    Mathlib.Tactic.BicategoryLike.Mor₂Iso →
                      Mathlib.Tactic.BicategoryLike.Mor₁ → m Mathlib.Tactic.BicategoryLike.Mor₂Iso) →
                  (horizontalCompM :
                      Mathlib.Tactic.BicategoryLike.Mor₂Iso →
                        Mathlib.Tactic.BicategoryLike.Mor₂Iso → m Mathlib.Tactic.BicategoryLike.Mor₂Iso) →
                    (symmM : Mathlib.Tactic.BicategoryLike.Mor₂Iso → m Mathlib.Tactic.BicategoryLike.Mor₂Iso) →
                      (coherenceCompM :
                          Mathlib.Tactic.BicategoryLike.CoherenceHom →
                            Mathlib.Tactic.BicategoryLike.Mor₂Iso →
                              Mathlib.Tactic.BicategoryLike.Mor₂Iso → m Mathlib.Tactic.BicategoryLike.Mor₂Iso) →
                        motive
                          { associatorM := associatorM, leftUnitorM := leftUnitorM, rightUnitorM := rightUnitorM,
                            id₂M := id₂M, coherenceHomM := coherenceHomM, comp₂M := comp₂M,
                            whiskerLeftM := whiskerLeftM, whiskerRightM := whiskerRightM,
                            horizontalCompM := horizontalCompM, symmM := symmM, coherenceCompM := coherenceCompM }) →
      (t : Mathlib.Tactic.BicategoryLike.MonadMor₂Iso m) → motive t