You're right: the set of morphisms is naturally a "bi-fibered" set over the set of objects. But the question we have to answer in the present case is "what do we put in the Slot "Base" of a category". This is less a matter of profound mathematical nature (I wrote often enough the uneasiness I have regarding extensible structures being "nonmathematical") than a matter of convenience and practical applications. Since I admit I am not a big contributor, I leave it to more experienced users to decide the best coding. I'll have a look at ( Arrow ` C ) as you suggested.
By the way: it is not because the set of morphisms is bi-fibered that we cannot consider it as a set: after all, "the total space of a fibration" is a common mathematical object. A special example: in a Lie groupoid, one requires that the morphisms form a smooth manifold: even if this manifold is bi-fibered, it is considered as a whole. About your wish that there be a "unique canonical notion of morphism once one knows the objects" (if I understood you correctly), it is not the case. It might be the case for algebraic structures concrete over Set, but not in general. Already when the objects are sets, the morphisms can be either functions or relations. When the objects are metric spaces, the best notion of morphisms is probably short maps (as hinted in my previous message in this thread), but the categories of metric spaces and continuous (or uniform, or Lipschitz, or locally Lipshitz, or coarse) maps are also interesting. Same goes with Banach spaces, etc. Even for structures, it is not that clear: tropical semiring, p-adic valuations (by the way: your formalization of Ostrowski is impressive), etc. Benoît -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/3fce3f5e-3fc6-4b15-b024-1f51fbe54016%40googlegroups.com.
