Post #1816231

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