proposition: Lemma projected_monoid : IsMonoid B.
proof: Proof. split. - apply (projected_sg f). assumption. - repeat intro; apply (injective f). rewrite op_correct, unit_correct, left_identity. reflexivity. - repeat intro; apply (injective f). rewrite op_correct, unit_correct, right_identity. reflexivity. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra