diff --git a/contrib/HoTTBook.v b/contrib/HoTTBook.v
index b883cd43ae9..c3252c9336f 100644
--- a/contrib/HoTTBook.v
+++ b/contrib/HoTTBook.v
@@ -58,7 +58,7 @@
 *)
 
 From HoTT Require Import Basics Truncations.
-From HoTT Require Idempotents Spaces.Spheres Spaces.No Spaces.Nat.
+From HoTT Require Idempotents Spaces.No Spaces.Nat.
 From HoTT Require HIT.V HIT.Flattening Homotopy.WhiteheadsPrinciple Homotopy.Hopf.
 From HoTT Require Categories.
 From HoTT Require Metatheory.IntervalImpliesFunext Metatheory.UnivalenceImpliesFunext.
diff --git a/contrib/SetoidRewrite.v b/contrib/SetoidRewrite.v
index d905e50362e..aa1520a73de 100644
--- a/contrib/SetoidRewrite.v
+++ b/contrib/SetoidRewrite.v
@@ -11,11 +11,11 @@ All files that import WildCat/SetoidRewrite.v will also recursively import the e
 (** Because of this, this file needs to be the *first* file Require'd in any file that uses it.  Otherwise, the typeclasses hintdb is cleared, breaking typeclass inference.  Moreover, if Foo Requires this file, then Foo must also be the first file Require'd in any file that Requires Foo, and so on. In the long term it would be good if this could be avoided.*)
 
 From Coq Require Init.Tactics.
-From HoTT Require Import Basics.Overture Basics.Tactics.
+From HoTT Require Import Basics.Overture.
 From HoTT Require Import Types.Forall.
 From Coq Require Setoids.Setoid.
 Import CMorphisms.ProperNotations.
-From HoTT Require Import WildCat.Core WildCat.Bifunctor WildCat.Prod
+From HoTT Require Import WildCat.Core
   WildCat.NatTrans WildCat.Equiv.
 
 #[export] Instance reflexive_proper_proxy {A : Type}
diff --git a/theories/Algebra/AbGroups/AbPushout.v b/theories/Algebra/AbGroups/AbPushout.v
index 5af7dd66b52..0f89c933c0d 100644
--- a/theories/Algebra/AbGroups/AbPushout.v
+++ b/theories/Algebra/AbGroups/AbPushout.v
@@ -1,4 +1,4 @@
-Require Import Basics Types Truncations.Core Modalities.ReflectiveSubuniverse.
+Require Import Basics Types Truncations.Core.
 Require Import WildCat.Core HSet.
 Require Export Algebra.Groups.Image Algebra.Groups.QuotientGroup.
 Require Import AbGroups.AbelianGroup AbGroups.Biproduct.
diff --git a/theories/Algebra/AbGroups/Abelianization.v b/theories/Algebra/AbGroups/Abelianization.v
index e49a7cb237b..515f74a89b5 100644
--- a/theories/Algebra/AbGroups/Abelianization.v
+++ b/theories/Algebra/AbGroups/Abelianization.v
@@ -1,7 +1,6 @@
 Require Import Basics Types Truncations.Core.
 Require Import Cubical WildCat.
 Require Import Colimits.Coeq.
-Require Import Algebra.Groups.Group.
 Require Import Algebra.AbGroups.AbelianGroup.
 Require Import Modalities.ReflectiveSubuniverse.
 
diff --git a/theories/Algebra/Congruence.v b/theories/Algebra/Congruence.v
index f344ecb9109..5c8ba28c89b 100644
--- a/theories/Algebra/Congruence.v
+++ b/theories/Algebra/Congruence.v
@@ -1,4 +1,4 @@
-Require Import Classes.interfaces.abstract_algebra.
+Require Import Classes.interfaces.canonical_names.
 
 (* We say that a relation is a congruence if it respects the operation.
   This is technically incorrect since we are not enforcing the relation to be an equivalence relation.
diff --git a/theories/Algebra/Groups/Group.v b/theories/Algebra/Groups/Group.v
index 02c353498af..326a7aa83af 100644
--- a/theories/Algebra/Groups/Group.v
+++ b/theories/Algebra/Groups/Group.v
@@ -1,6 +1,6 @@
 Require Import Basics Types HProp HFiber HSet.
 Require Import PathAny.
-Require Import (notations) Classes.interfaces.abstract_algebra.
+Require Import (notations) Classes.interfaces.canonical_names.
 Require Export (hints) Classes.interfaces.abstract_algebra.
 Require Export (hints) Classes.interfaces.canonical_names.
 (** We only export the parts of these that will be most useful to users of this file. *)
diff --git a/theories/Algebra/Rings/CRing.v b/theories/Algebra/Rings/CRing.v
index ec1c80df1b2..d2334839d6b 100644
--- a/theories/Algebra/Rings/CRing.v
+++ b/theories/Algebra/Rings/CRing.v
@@ -1,5 +1,4 @@
 Require Import WildCat.
-Require Import Spaces.Nat.Core.
 (* Some of the material in abstract_algebra and canonical names could be selectively exported to the user, as is done in Groups/Group.v. *)
 Require Import Classes.interfaces.abstract_algebra.
 Require Import Algebra.AbGroups.
diff --git a/theories/Algebra/Rings/ChineseRemainder.v b/theories/Algebra/Rings/ChineseRemainder.v
index 57928822193..788ba59a8cc 100644
--- a/theories/Algebra/Rings/ChineseRemainder.v
+++ b/theories/Algebra/Rings/ChineseRemainder.v
@@ -1,4 +1,4 @@
-Require Import Classes.interfaces.abstract_algebra.
+Require Import Classes.interfaces.canonical_names.
 Require Import WildCat.
 Require Import Modalities.ReflectiveSubuniverse.
 Require Import Algebra.AbGroups.
diff --git a/theories/Algebra/Rings/Ideal.v b/theories/Algebra/Rings/Ideal.v
index cfe1f7fa125..f6defbae06b 100644
--- a/theories/Algebra/Rings/Ideal.v
+++ b/theories/Algebra/Rings/Ideal.v
@@ -1,6 +1,6 @@
 Require Import Basics Types.
 Require Import Spaces.Finite.Fin.
-Require Import Classes.interfaces.abstract_algebra.
+Require Import Classes.interfaces.canonical_names.
 Require Import Algebra.Rings.Ring.
 Require Import Algebra.AbGroups.
 
diff --git a/theories/Algebra/Rings/Z.v b/theories/Algebra/Rings/Z.v
index 714930fc69c..97f31954f95 100644
--- a/theories/Algebra/Rings/Z.v
+++ b/theories/Algebra/Rings/Z.v
@@ -1,4 +1,4 @@
-Require Import Classes.interfaces.abstract_algebra.
+Require Import Classes.interfaces.canonical_names.
 Require Import Algebra.AbGroups.
 Require Import Algebra.Rings.CRing.
 Require Import Spaces.Int Spaces.Pos.
diff --git a/theories/Algebra/Universal/Algebra.v b/theories/Algebra/Universal/Algebra.v
index 6e6f67ed721..a7c6c624736 100644
--- a/theories/Algebra/Universal/Algebra.v
+++ b/theories/Algebra/Universal/Algebra.v
@@ -7,8 +7,7 @@ Local Unset Elimination Schemes.
 Require Export HoTT.Basics.
 
 Require Import
-  HoTT.Types
-  HoTT.HSet.
+  HoTT.Types.
 
 Declare Scope Algebra_scope.
 Delimit Scope Algebra_scope with Algebra.
diff --git a/theories/Categories/Category/Pi.v b/theories/Categories/Category/Pi.v
index a9afc27ebc9..5a9ad06b423 100644
--- a/theories/Categories/Category/Pi.v
+++ b/theories/Categories/Category/Pi.v
@@ -1,7 +1,6 @@
 (** * Dependent Product Category *)
 Require Import Category.Strict.
 Require Import Basics.Trunc.
-Require Import Types.Forall.
 
 Set Universe Polymorphism.
 Set Implicit Arguments.
diff --git a/theories/Categories/GroupoidCategory/Core.v b/theories/Categories/GroupoidCategory/Core.v
index e567b2a9e23..e5f3adc96d1 100644
--- a/theories/Categories/GroupoidCategory/Core.v
+++ b/theories/Categories/GroupoidCategory/Core.v
@@ -1,6 +1,6 @@
 (** * Groupoids *)
 Require Import Category.Morphisms Category.Strict.
-Require Import Trunc Types.Forall PathGroupoids Basics.Tactics.
+Require Import Trunc PathGroupoids Basics.Tactics.
 
 Set Universe Polymorphism.
 Set Implicit Arguments.
diff --git a/theories/Classes/implementations/field_of_fractions.v b/theories/Classes/implementations/field_of_fractions.v
index c1c2d1529af..876570370d5 100644
--- a/theories/Classes/implementations/field_of_fractions.v
+++ b/theories/Classes/implementations/field_of_fractions.v
@@ -1,4 +1,4 @@
-Require Import HoTT.HIT.quotient HoTT.Basics.Trunc.
+Require Import HoTT.HIT.quotient.
 Require Import 
   HoTT.Classes.interfaces.abstract_algebra
   HoTT.Classes.theory.dec_fields.
diff --git a/theories/Classes/implementations/list.v b/theories/Classes/implementations/list.v
index 10ad86180b4..89cb74a8d7b 100644
--- a/theories/Classes/implementations/list.v
+++ b/theories/Classes/implementations/list.v
@@ -1,5 +1,5 @@
 Require Import
-  HoTT.Classes.interfaces.abstract_algebra.
+  HoTT.Classes.interfaces.canonical_names.
 
 Generalizable Variables A B C.
 
diff --git a/theories/Classes/implementations/natpair_integers.v b/theories/Classes/implementations/natpair_integers.v
index bed5e63fdef..1a5bbe73d35 100644
--- a/theories/Classes/implementations/natpair_integers.v
+++ b/theories/Classes/implementations/natpair_integers.v
@@ -1,5 +1,5 @@
 Require Import HoTT.HIT.quotient
-  HoTT.TruncType HoTT.Basics.Trunc.
+  HoTT.TruncType.
 Require Import
   HoTT.Classes.implementations.peano_naturals
   HoTT.Classes.interfaces.abstract_algebra
diff --git a/theories/Classes/interfaces/ua_algebra.v b/theories/Classes/interfaces/ua_algebra.v
index 4ca840bc655..d63f38f37f3 100644
--- a/theories/Classes/interfaces/ua_algebra.v
+++ b/theories/Classes/interfaces/ua_algebra.v
@@ -8,7 +8,6 @@ Require Export
 
 Require Import
   HoTT.Types
-  HoTT.HSet
   HoTT.Classes.implementations.list.
 
 Import ne_list.notations.
diff --git a/theories/Classes/theory/additional_operations.v b/theories/Classes/theory/additional_operations.v
index 69857a5311b..bb6ae2b264b 100644
--- a/theories/Classes/theory/additional_operations.v
+++ b/theories/Classes/theory/additional_operations.v
@@ -1,4 +1,4 @@
-Require Import HoTT.Classes.interfaces.abstract_algebra.
+Require Import HoTT.Classes.interfaces.canonical_names.
 
 Generalizable Variables A R.
 
diff --git a/theories/Classes/theory/ua_first_isomorphism.v b/theories/Classes/theory/ua_first_isomorphism.v
index e1ecd7526a6..d9492e4f549 100644
--- a/theories/Classes/theory/ua_first_isomorphism.v
+++ b/theories/Classes/theory/ua_first_isomorphism.v
@@ -6,7 +6,6 @@
 Require Import
   HSet
   Colimits.Quotient
-  Modalities.ReflectiveSubuniverse
   Classes.interfaces.canonical_names
   Classes.theory.ua_isomorphic
   Classes.theory.ua_subalgebra
diff --git a/theories/Classes/theory/ua_prod_algebra.v b/theories/Classes/theory/ua_prod_algebra.v
index cd3cae13edf..275a2656f0d 100644
--- a/theories/Classes/theory/ua_prod_algebra.v
+++ b/theories/Classes/theory/ua_prod_algebra.v
@@ -1,6 +1,5 @@
 Require Import
   HoTT.Types.Bool
-  HoTT.Types.Forall
   HoTT.Classes.theory.ua_homomorphism.
 
 Import algebra_notations ne_list.notations.
diff --git a/theories/Colimits/Coeq.v b/theories/Colimits/Coeq.v
index aa958eb9b58..364d0c0bac6 100644
--- a/theories/Colimits/Coeq.v
+++ b/theories/Colimits/Coeq.v
@@ -1,6 +1,5 @@
 Require Import Basics.
 Require Import Types.Paths Types.Arrow Types.Sigma Types.Forall Types.Universe Types.Prod.
-Require Import Cubical.DPath.
 Require Import Colimits.GraphQuotient.
 
 Local Open Scope path_scope.
diff --git a/theories/Colimits/GraphQuotient.v b/theories/Colimits/GraphQuotient.v
index 853c422368f..345a7cd9a9d 100644
--- a/theories/Colimits/GraphQuotient.v
+++ b/theories/Colimits/GraphQuotient.v
@@ -1,5 +1,5 @@
 Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Equivalences.
-Require Import Types.Universe Types.Paths Types.Arrow Types.Sigma Types.Forall Cubical.DPath.
+Require Import Types.Universe Types.Paths Types.Arrow Types.Sigma Cubical.DPath.
 
 (** * Quotient of a graph *)
 
diff --git a/theories/HIT/surjective_factor.v b/theories/HIT/surjective_factor.v
index 21c46c02112..d3b0d5c46cd 100644
--- a/theories/HIT/surjective_factor.v
+++ b/theories/HIT/surjective_factor.v
@@ -1,5 +1,4 @@
 Require Import
-        HoTT.Types
         HoTT.Basics
         HoTT.Truncations.Core Modalities.Modality.
 
diff --git a/theories/HSet.v b/theories/HSet.v
index 27450f4b126..3cadafe3f7a 100644
--- a/theories/HSet.v
+++ b/theories/HSet.v
@@ -1,6 +1,6 @@
 (* -*- mode: coq; mode: visual-line -*-  *)
 Require Import Basics.
-Require Import Types.Sigma Types.Forall Types.Paths Types.Unit Types.Arrow.
+Require Import Types.Sigma Types.Paths Types.Unit Types.Arrow.
 
 (** * H-Sets *)
 
diff --git a/theories/Homotopy/EMSpace.v b/theories/Homotopy/EMSpace.v
index fb6aefddca6..5f14e8b5aae 100644
--- a/theories/Homotopy/EMSpace.v
+++ b/theories/Homotopy/EMSpace.v
@@ -4,11 +4,9 @@ Require Import Cubical.DPath.
 Require Import Algebra.AbGroups.
 Require Import Homotopy.Suspension.
 Require Import Homotopy.ClassifyingSpace.
-Require Import Homotopy.HSpace.Core.
 Require Import Homotopy.HSpace.Coherent.
 Require Import Homotopy.HomotopyGroup.
 Require Import Homotopy.Hopf.
-Require Import TruncType.
 Require Import Truncations.Core Truncations.Connectedness.
 Require Import WildCat.
 
diff --git a/theories/NullHomotopy.v b/theories/NullHomotopy.v
index ee0b1831ec9..f6e9a4ecace 100644
--- a/theories/NullHomotopy.v
+++ b/theories/NullHomotopy.v
@@ -1,6 +1,6 @@
 (* -*- mode: coq; mode: visual-line -*- *)
 Require Import HoTT.Basics.
-Require Import Types.Sigma Types.Forall.
+Require Import Types.Sigma.
 Local Open Scope path_scope.
 
 
diff --git a/theories/Pointed/pModality.v b/theories/Pointed/pModality.v
index d3c9ba02338..36d340b2000 100644
--- a/theories/Pointed/pModality.v
+++ b/theories/Pointed/pModality.v
@@ -1,4 +1,4 @@
-Require Import Basics Types ReflectiveSubuniverse Pointed.Core Pointed.pEquiv.
+Require Import Basics Types ReflectiveSubuniverse Pointed.Core.
 
 Local Open Scope pointed_scope.
 
diff --git a/theories/PropResizing/ImpredicativeTruncation.v b/theories/PropResizing/ImpredicativeTruncation.v
index dc83e8cc104..9adbb46f105 100644
--- a/theories/PropResizing/ImpredicativeTruncation.v
+++ b/theories/PropResizing/ImpredicativeTruncation.v
@@ -1,7 +1,7 @@
 (* -*- mode: coq; mode: visual-line -*-  *)
 (** * Impredicative truncations. *)
 
-Require Import HoTT.Basics HoTT.Types.
+Require Import HoTT.Basics.
 Require Import PropResizing.PropResizing.
 Local Open Scope path_scope.
 
diff --git a/theories/Sets/AC.v b/theories/Sets/AC.v
index 1742cd67928..5a770400e68 100644
--- a/theories/Sets/AC.v
+++ b/theories/Sets/AC.v
@@ -1,4 +1,4 @@
-From HoTT Require Import ExcludedMiddle abstract_algebra.
+From HoTT Require Import ExcludedMiddle canonical_names.
 From HoTT Require Import HIT.unique_choice.
 From HoTT Require Import Spaces.Card.
 
diff --git a/theories/Spaces/Circle.v b/theories/Spaces/Circle.v
index 6acb5981ac0..ab93bcb41b0 100644
--- a/theories/Spaces/Circle.v
+++ b/theories/Spaces/Circle.v
@@ -5,7 +5,6 @@ Require Import HSet.
 Require Import Spaces.Pos Spaces.Int.
 Require Import Colimits.Coeq.
 Require Import Truncations.Core Truncations.Connectedness.
-Require Import Cubical.DPath.
 
 (** * Theorems about the [Circle]. *)
 
diff --git a/theories/Types/Forall.v b/theories/Types/Forall.v
index 22f65cc5094..7cc510a17dc 100644
--- a/theories/Types/Forall.v
+++ b/theories/Types/Forall.v
@@ -2,7 +2,7 @@
 (** * Theorems about dependent products *)
 
 Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids
-               Basics.Tactics Basics.Trunc Basics.Contractible.
+               Basics.Tactics Basics.Contractible.
 
 Require Export Basics.Trunc (istrunc_forall).
 
diff --git a/theories/Types/Sum.v b/theories/Types/Sum.v
index 864573cc080..ff6b8831666 100644
--- a/theories/Types/Sum.v
+++ b/theories/Types/Sum.v
@@ -4,7 +4,7 @@
 Require Import HoTT.Basics.
 Require Import Types.Empty Types.Unit Types.Prod Types.Sigma.
 (** The following are only required for the equivalence between [sum] and a sigma type *)
-Require Import Types.Bool Types.Forall.
+Require Import Types.Bool.
 
 Local Open Scope trunc_scope.
 Local Open Scope path_scope.
diff --git a/theories/WildCat/Monoidal.v b/theories/WildCat/Monoidal.v
index c3e6b80c442..7b145cc3dc5 100644
--- a/theories/WildCat/Monoidal.v
+++ b/theories/WildCat/Monoidal.v
@@ -1,4 +1,4 @@
-Require Import Basics.Overture Basics.Tactics.
+Require Import Basics.Overture.
 Require Import Types.Forall.
 Require Import WildCat.Core WildCat.Bifunctor WildCat.Prod WildCat.Equiv WildCat.NatTrans.
 
diff --git a/theories/WildCat/Products.v b/theories/WildCat/Products.v
index 83912cef8d3..1e54cd998d8 100644
--- a/theories/WildCat/Products.v
+++ b/theories/WildCat/Products.v
@@ -1,7 +1,7 @@
 Require Import Basics.Equivalences Basics.Overture Basics.Tactics.
 Require Import Types.Bool Types.Prod.
 Require Import WildCat.Bifunctor WildCat.Core WildCat.Equiv WildCat.EquivGpd
-               WildCat.Forall WildCat.NatTrans WildCat.Opposite WildCat.Prod
+               WildCat.Forall WildCat.NatTrans WildCat.Opposite
                WildCat.Universe WildCat.Yoneda WildCat.ZeroGroupoid.
 
 (** * Categories with products *)
diff --git a/theories/WildCat/ZeroGroupoid.v b/theories/WildCat/ZeroGroupoid.v
index fb95b36385d..62290fbfef3 100644
--- a/theories/WildCat/ZeroGroupoid.v
+++ b/theories/WildCat/ZeroGroupoid.v
@@ -1,6 +1,6 @@
-Require Import Basics.Overture Basics.Tactics Basics.Equivalences
+Require Import Basics.Overture Basics.Tactics
                Basics.PathGroupoids.
-Require Import WildCat.Core WildCat.Equiv WildCat.EquivGpd WildCat.Prod
+Require Import WildCat.Core WildCat.Equiv WildCat.EquivGpd
                WildCat.Forall.
 
 (** * The wild 1-category of 0-groupoids. *)