{P : Sort u_1} →
  {m : Type u → Type v} →
    {n : Type u → Type w} →
      {t : MonadFunctorT m n} →
        {m' : Type u → Type v} →
          {n' : Type u → Type w} →
            {t' : MonadFunctorT m' n'} → m = m' → n = n' → t ≍ t' → MonadFunctorT.noConfusionType P t t'