Duplicated notation for category exponential

Stream: mathlib4

[Bhavik Mehta]

For cartesian closed categories, we currently have two notations for the exponential: A ⟹ B or B ^^ A. The latter of these is barely used (only once throughout mathlib), is available in the global context, and clashes with xor on Booleans. I don't think this should be in a global scope, and I'm not even sure it should exist at all. How would people feel about removing the latter?

Aside: mathlib3#2894 shows this was my fault all along!

[Joël Riou]

I feel we may safely remove "^^".