{m : Type u → Type v} →
  {n : Type u → Type w} →
    {P : Sort u_1} →
      {monadMap monadMap' : {α : Type u} → ({β : Type u} → m β → m β) → n α → n α} →
        { monadMap := monadMap } = { monadMap := monadMap' } → (monadMap ≍ monadMap' → P) → P