UniMath
UniMath copied to clipboard
UniMath
Category of `grs` does not have the right hom-types
in CT.categories.grs, morphisms of groups are defined to be monoid morphisms - probably this is a trick with the goal of making the proof of univalence easier.
While this is technically doable, the fact that such a morphism preserves inverses should be available - either as part of the definition, or as a lemma.
I would prefer the former: preservation of inverses should be part of the definition.
Also, grs is not a good name for the category of groups - the identifier and the file need to be renamed.
Good ideas.
To be explicit - "grs" is not a good name because it's not a word or concatenation of words.
On 08/02/18 14:41, Daniel R. Grayson wrote:
Good ideas.
To be explicit - "grs" is not a good name because it's not a word or concatenation of words.
grp would be acceptable to me despite not being a word, since that is
a commonly used name for the category of groups.
One convention one could have is using grp for the type, and Grp for
the category, of groups, and similar for other structures. Or a
variation on that.
I like using capitalized words for types exclusively. Categories don't pervade UniMath, after all. Group for the type of groups and GroupCat for the category of groups seem good.
As a side note, Algebra/Monoids_and_Groups.v did not define a type for group morphisms; instead it just develops properties of monoid morphisms between groups. Also the fact that such morphisms preserve inverses is a lemma named monoidfuninvtoinv there.
Considering that the fact that monoid morphisms must preserve inverses is available as a lemma (monoidfuninvtoinv), it doesn't seem necessary to me to separately define group homomorphisms with inverse preservation in their definition. After all, what would be the criterion for when to include consequences of definitions in the definitions themselves? I would say it shouldn't be done at all.
In other words, I think this is fine as-is.
