Here is a question prompted by my remark in https://groups.google.com/d/msg/metamath/Nvh_ue-PSBM/Nj-XpBvBAAAJ "there is some gymnastic to do to put things in the right "slot", which looks painful..."
I see in ~df-cat that if c is a category, then ( Base " c ) is actually the set of objects of c while the set of morphisms is denoted ( Hom " c ). It looks a bit strange, and it would be more natural in my opinion to take the set of morphisms as the base set, while having a slot ( Obj " c ) for the set of objects of c. Is there a particular reason for choosing the current convention ? Would it be possible to change it to the proposed one, or would it be too much work ? 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/12352990-c8ab-4df9-b031-d30c586b7ef8%40googlegroups.com.
