I figured the monoid example would come up, but I think that really is a special case. Morphisms don't really act like a set, they are more like a |C| x |C| indexed family of sets. It just so happens that when |C| is a singleton that's just one set. In any other case, in any category that is not just a monoid in disguise, collapsing all morphisms into one pot doesn't look like the right thing to do. (Yes it is useful for some things, and (Arrow`C) is available for that, but most of the time when you want to build hom sets you really want the domain and codomain to be inputs not outputs.) So even if we wanted the homs to be "primary", they don't have the right type to be in the (Base`C) slot anyway.
I think that "the morphisms are obvious" given the objects in the same way that the addition or multiplication is obvious given the base set like RR or CC. You can call it an "abuse of language", but I think this is really what mathematicians want structures to accomplish, and which is encoded in systems like Lean's typeclass inference, that infers a quasi-unique structure "ring R" given a carrier type R. (Mathematically it is clearly not unique in most cases - there are many ring structures on RR - but we really want a single "canonical" one.) On Thu, Jan 30, 2020 at 6:36 PM Benoit <[email protected]> wrote: > Ok. I'm not insisting since I'm not fond of extensible structures anyway. > But it is certainly not odd to make morphisms the underlying set of a > category. The fact that an "arrows only" definition of a category is > possible shows that it's that latter set which is more important. Also, it > is common to say that a monoid (resp. group) is a category (resp. groupoid) > with one object. (This is actually what led me to this proposal, see the > linked post with the question by David Starner.) > > Indeed, one often says things like "the category of groups" instead of > "the category of groups and group morphisms" or "the category of > morphisms", but this is an abuse of language. It's ok in this case since > the morphisms are obvious, but it is not always so. > > As you noted, considering posets as thin categories seems to contradict > this. The same goes with metric spaces as (\R, \leq)-enriched categories. > But actually, these are examples of categorification, so it's expected that > there is a shift by 1 (from n-morphisms to (n+1)-morphisms). > > 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/84285818-c976-4912-a4bd-2c9af466e79e%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/84285818-c976-4912-a4bd-2c9af466e79e%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAFXXJSssc1Kj0aifbfch4bzp5bD6cKPmpMBh3C3hiBbe7oKZMw%40mail.gmail.com.
