UniMath
definition of subgroup
Consider this:
I propose to start more gently, with words, and to say that a subgroup of G is a monomorphism from a group to G. After that, to introduce the type of subgroups, but using "being a monomorphism" as the property. If that particular form of the property (
) is needed somewhere, then we should add a fourth condition to this lemma:
My understanding is that we are to embrace the geometrical point of view given by the Galois theory of covering spaces. With this point of view, it makes more sense to define a subgroup as a connected set bundle and subsequently invoke 4.9.3 to prove that it corresponds to a monomorphism. (Btw, this lemma 4.9.3 is relatively new and was added to be able to talk about monos before subgroups are introduced.)
Oh, thanks.
I guess you mean a subgroup of G is a connected pointed set bundle over BG.
Definition 5.1.1 above posits that the fiber of Bf over the base point is a set. Another way to do it is to posit that Bf is a set bundle over BG. The two conditions are equivalent.
Is there a common view about which way is better?
Oh, thanks.
I guess you mean a subgroup of G is a connected pointed set bundle over BG.
Yes, thanks for the correction.
Definition 5.1.1 above posits that the fiber of Bf over the base point is a set. Another way to do it is to posit that Bf is a set bundle over BG. The two conditions are equivalent.
Is there a common view about which way is better?
The same happens in the definition of a pointed connected groupoid (former definition of group) and the convention there was to state dependent propositions on the point (or the designated shape I should now say) only. We should stick to this convention I suppose. (it has the advantage of making definitions shorter, avoiding a Pi.)
That being said, here def 5.1.1 is indeed a little different (in the form) than pointed connected set bundle, as it limits (a priori) the total space of the bundle to a groupoid. Of course the base being a groupoid it is provable that the total space of any set bundle is also a groupoid, so both definitions are equivalent, but as it is def 5.1.1 seems "in between" the mono version and the geometrical version.