the trouble with general theories of abstract nonsense is the "general abstract nonsense" part
I've been doing some category theory lately. Finally got a half-decent grasp on duality & exponentials, and I've been wondering: what is a coexponential?
If, in the category C, every morphism "g" from the product of X and Y to Z yields a morphism "lambda-g" from X to Z to the power of Y (such that a certain diagram commutes), we get a very strange construct in the opposite category:
For every morphism "g" from Z to the sum of X and Y, there is a "lambda-g" from Z-sub-Y to X, such that a certain diagram commutes. In this context, the "eval" morphism goes from Z to Z-sub-Y plus Y, and the sum of lambda-g with 1 on eval must equal g.
Of course, I like a set-theoretic (or type-theoretic, as the case may be) interpretation as much as the next guy. However, for this to make sense, eval has to send every value in Z to either itself in Z-sub-Y or to the value in Y that g would send it to. That's all fine and dandy until you realize that eval can't depend on g.
Whil I do think the "without" interpretation ought to work, I just can't quite wrap my head around it.