I'm trying again to prove stuff in metamath, starting with the "definition" of a group in Algebra: Chapter 0, by Paolo Aluffi: "A group is a groupoid with a single object." After pushing through the category theory section, I've finally put together:
$( <MM> <PROOF_ASST> THEOREM=catisoismnd LOC_AFTER= hd1:: |- ( ph -> B = ( Base ` C ) ) hd2:: |- ( ph -> .x. = ( comp ` C ) ) hd3:: |- ( ph -> I = ( Iso ` C ) ) hd4:: |- ( ph -> C e. Cat ) hd5:: |- ( ph -> suc (/) ~~ B ) hd6:: |- ( ph -> I = ( Base ` G ) ) hd7:: |- ( ph -> .x. = ( +g ` G ) ) qed:: |- ( ph -> G e. Mnd ) That is, if I understand it right, the isomorphisms of a category with one object form a monoid. Am I on the right track? -- Kie ekzistas vivo, ekzistas espero. -- 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/CAMZ%3Dzj4YYePF6bCiqw1%2BXTiegLH-V3yygSLZV_0Ltr%3DDCHR-2A%40mail.gmail.com.
