I think this is a perfect example of when something is or is not an explanation. It's both in this case: to the cogniscenti, it is perfectly clear; the novice is going to head off on the wrong track. On 4/30/11 15:58, Charles Wells wrote:
In the expression "any x:T->X" the T depends on x. If you use the arrow notation you seem bound to name the domain of the morphism. You could say "for any x with codomain X there is an e:dom x -> X ..." but in the rest of the sentence you will have to mention the domain again.
My impression is that notation "any x:T->X" where T depends on x without that fact being mentioned is common in category theory writing. There is nothing wrong with this if a reader understands the intent. <snip>
-- Dr. D. E. Stevenson Associate Professor Director, Insitute for Modeling and Simulation Applications School of Computing, Clemson University [For admin and other information see: http://www.mta.ca/~cat-dist/ ]