Hello! David Leduc is not satisfied:
Take any category E where exponentiable is interesting. Then the dual of exponentiable is not boring in E^op.
Indeed! And this is clearly true of the example given by Thomas, namely Set^op.
However, I am not yet satisfied. Let me precise my thoughts. In the textbooks and lecture notes on category category that I have read, there are always product and coproduct, pullback and pushout, equalizer and coequalizer, monomorphism and epimorphism, and so on. However exponential is always left alone. That is why I assumed it is boring. If it is not boring, why is it never mentioned in textbooks and lecture notes on category theory?
I wonder whether it makes sense to introduce notions, which only in the duals of familiar categories. Of course, Set^op is equivalent to the category of complete atomic Boolean algebras, but I do not see that the dual of exponentiation plays an important role in the theory if these Boolean algebras.
Also, in logic, "and" goes in pair with "or", "for all" goes in pair with "there exists". But implication is always left alone. Why is it
In classical logic, one can form this "co-implication" but it does not look very interesting to me. In intuitionistic logic I do not see how to add it more ore less meaningfully (e.g. in such a way that it is left adjoint to "or" in the first argument). Greetings Reinhard [For admin and other information see: http://www.mta.ca/~cat-dist/ ]