proposition: Lemma projected_sl: IsSemiLattice B.
proof: Proof. split. - apply (projected_com_sg f). assumption. - repeat intro; apply (injective f). rewrite !op_correct, (idempotency (+) _). reflexivity. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.theory.groups