diff --git a/group_theory/basic.hlean b/group_theory/basic.hlean
index 1cca2da..1419ba1 100644
--- a/group_theory/basic.hlean
+++ b/group_theory/basic.hlean
@@ -10,13 +10,12 @@ Basic group theory
 /-
   Groups are defined in the HoTT library in algebra/group, as part of the algebraic hierarchy.
   However, there is currently no group theory.
-  The only relevant defintions are the trivial group (in types/unit) and some files in algebra/
 -/
 
-import algebra.group types.pointed types.pi
+import types.pointed types.pi algebra.bundled
 
 open eq algebra pointed function is_trunc pi
-
+set_option class.force_new true
 namespace group
 
   definition pointed_Group [instance] (G : Group) : pointed G := pointed.mk one
diff --git a/group_theory/constructions.hlean b/group_theory/constructions.hlean
index 6f6b558..39dd861 100644
--- a/group_theory/constructions.hlean
+++ b/group_theory/constructions.hlean
@@ -10,6 +10,7 @@ import .basic hit.set_quotient types.sigma types.list types.sum
 
 open eq algebra is_trunc set_quotient relation sigma sigma.ops prod prod.ops sum list trunc function
      equiv
+set_option class.force_new true
 namespace group
 
   /- Subgroups -/