Post #1816232

@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.