A HoTT exercise: let \( A \) be a type with a binary operation \( * : A \to A \to A \). Suppose that \( * \) is associative, commutative, and idempotent, in the sense that \( \Pi_{a\, b\, c : A} a * (b * c) = (a * b) * c \), \( \Pi_{a\, b : A} a * b = b * a \) and \( \Pi_{a : A} a * a = a \). Show that \( A \) is an hset (and hence a semilattice in the ordinary sense).