Re: [HoTT] Identity versus equality

[Michael Shulman <shu...@sandiego.edu>]

On Sun, May 10, 2020 at 9:51 AM Nicolai Kraus <nicola...@gmail.com> wrote:
> It's easy to change the second definition to
> define infinity groups instead of 1-groups (see e.g. arXiv:1802.04315 ,
> arXiv:1805.02069, and Ulrik's comment). But it's unclear whether there
> is a nice way for the first definition.

On the other hand, it's easy to change the first definition to define
monoids/semigroups/rings/fields/lattices/universal-algebras/etc., and
impossible to do the same for the second.  I think the fact that
groups are part of the general theory of algebraic structures on sets
is more important to incorporate in a definition.  The equivalence
between groups and connected pointed 1-types is better viewed as a
theorem than a definition.

And hence, the "definition" of oo-groups as connected pointed types is
more of a hack than a true definition.  In an ideal world, that would
be a theorem too.  (And the corresponding theorem in classical
mathematics has important content: there are important oo-groupoids
that are obtained by delooping oo-groups nontrivially.)