First note that categories as defined in set.mm are small (that is, their
morphisms form sets), so there is no size issue to worry about.
I would prove the following statements:
* the set of isomorphisms of a category is a groupoid;
* the set of endomorphisms of a category on a given object is a monoid;
* the set of automorphisms of a category on a given object is a group.
The easiest way to code these is probably to use the restriction of
extensible structures, |`s(see df-ress). Therefore it would look something
like:
${
$e |- ( ph -> C e. Cat ) $.
$p |- ( ph -> ( C |`s ( Iso `C ) ) e. Groupoid ) $= ? $.
$e |- ( ph -> X e. ( Base `C ) ) $.
$p |- ( ph -> ( C |`s ( ( End ` C ) ` X ) ) e. Monoid ) $= ? $.
$p |- ( ph -> ( C |`s ( ( Aut `C ) `X ) ) e. Group ) $= ? $.
$}
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/394bb6cf-3adf-467b-992a-6129555bd233%40googlegroups.com.
