chore(category_theory/closed/cartesian): make exp right-associative (#11172)
chore(category_theory/closed/cartesian): make exp right-associative (#11172)

This makes `X ⟹ Y ⟹ Z` parse as `X ⟹ (Y ⟹ Z)`, like ordinary function types.





leanprover-community/mathlib,leanprover-community/mathlib