{G} : Subgroup G. Proof. rapply (Build_Subgroup' (fun x => x = mon_unit)). 1: reflexivity. intros x y p q. rewrite p, q. rewrite left_identity. apply negate_mon_unit. Defined.
Require Import Basics Types HFiber WildCat.Core. Require Import Truncations.Core. Require Import Algebra.Groups.Group TruncType.