Post #1816230

2026-02-24 23:29 UTC

@MartinEscardo I had the impression you had written some answer to my message, which I can't find back. Anyway, what I meant is that one could wish to define a group in HoTT by considering a type G plus a binary law G × G → G, plus a member e:G, plus the equalities that say that the law is associative and e is neutral. But the HoTT book, or Rijke's book, insist that G be a *set*. On the other hand, it seems that the Symmetry book (work in project of Marc Bezem, Ulrik Buchholtz, Pierre Cagne, Bjørn Ian Dundas, Daniel R. Grayson) take a more general definition and really study cases where G might have higher structure. https://unimath.github.io/SymmetryBook/book.pdf

Replies (2)

@MartinEscardo@mathstodon.xyz 2026-02-24 23:59

@antoinechambertloir I see what you mean now. A group, by conception, must be a set. But you may also wish to consider types equipped with group structure (and then coherence laws). These are called *higher* groups. We are not ruling out higher groups. We are just reserving the terminology "group" for the traditional notion, and distinguishing it from the new notion by adding "higher" as an adjective. So saying "there are no higher semilattices" really means that any type equipped with semilattice structure must be a set (theorem!). (And, a remark, usually when we move from sets to arbitrary types, regarding algebraic structrures, we need to consider coherences (equations between equations). But, in this case, no coherences are needed in order to show that we actually get a set.)

Open ##1816231
@oantolin@mathstodon.xyz 2026-02-25 02:43

@antoinechambertloir The definition you give of group, which is just like the normal one,but without asking that G be a set, is studied in algebraic topology under the name "H-group" or "grouplike H-space" (you might think the H is for "homotopy" but it's actually for Hopf!). There is an even fancier notion that includes coherence data called a "grouplike A_infinity-space" or a "grouplike E_1-space" which is equivalent to being a loop space, and which HoTT people call a "higher group". So, (1) people (mostly homotopy theorists) do study analogues of algebraic structures where the underlying "set" is a homotopy type, (2) as the example of groups shows, the definitions for sets split into more than one definition depending on how much coherence data you want to include. A definition can even split into infinitely many definitions: I mentioned "A_infinity-spaces" above but there are also "A_n-spaces" for each finite n. EDIT: Sorry, @MartinEscardo, I meant to reply to Antoine's comment above, not to your reply to that comment.

Open ##1816232