∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T₁ T₂ : CategoryTheory.Monad C} [inst_1 : SizeOf C]
  (toNatTrans : CategoryTheory.NatTrans T₁.toFunctor T₂.toFunctor)
  (app_η :
    autoParam (∀ (X : C), CategoryTheory.CategoryStruct.comp (T₁.η.app X) (toNatTrans.app X) = T₂.η.app X)
      CategoryTheory.MonadHom.app_η._autoParam)
  (app_μ :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (T₁.μ.app X) (toNatTrans.app X) =
          CategoryTheory.CategoryStruct.comp
            (CategoryTheory.CategoryStruct.comp (T₁.map (toNatTrans.app X)) (toNatTrans.app (T₂.obj X))) (T₂.μ.app X))
      CategoryTheory.MonadHom.app_μ._autoParam),
  sizeOf { toNatTrans := toNatTrans, app_η := app_η, app_μ := app_μ } = 1 + sizeOf toNatTrans