{G} : Subgroup G. Proof. rapply (Build_Subgroup G (fun x => Unit)). split; auto; exact _. Defined.
Require Import Basics Types HFiber WildCat.Core. Require Import Truncations.Core. Require Import Algebra.Groups.Group TruncType.