Post #1816229

2026-02-23 21:17 UTC

@MartinEscardo @dwarn I like this, because it does not seem clear to me that once algebra is done within hott, every basic algebraic structure should a priori be a set. Maybe it's because higher groups are much more complicated than classical groups, but still.

Replies (1)

@antoinechambertloir@mathstodon.xyz 2026-02-24 23:29

@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

Open ##1816230