HoTT · jdchristensen · Sep 19, 2025 · Sep 17, 2025 · Sep 17, 2025 · Sep 17, 2025
diff --git a/theories/Algebra/AbGroups/AbHom.v b/theories/Algebra/AbGroups/AbHom.v
@@ -1,4 +1,4 @@
-Require Import Basics Types.
+From HoTT Require Import Basics Types.
 Require Import WildCat HSet Truncations.Core Modalities.ReflectiveSubuniverse.
 Require Import Groups.Group Groups.QuotientGroup AbelianGroup Biproduct.
 

diff --git a/theories/Algebra/AbGroups/AbProjective.v b/theories/Algebra/AbGroups/AbProjective.v
@@ -1,4 +1,4 @@
-Require Import Basics Types AbelianGroup AbPullback
+From HoTT Require Import Basics Types AbelianGroup AbPullback
   WildCat.Core Limits.Pullback ReflectiveSubuniverse Truncations.Core.
 
 (** * Projective abelian groups *)

diff --git a/theories/Algebra/AbGroups/AbPullback.v b/theories/Algebra/AbGroups/AbPullback.v
@@ -1,4 +1,4 @@
-Require Import Basics.
+From HoTT Require Import Basics.
 Require Import Limits.Pullback Cubical.PathSquare.
 Require Export Algebra.Groups.GrpPullback.
 Require Import Algebra.AbGroups.AbelianGroup.

diff --git a/theories/Algebra/AbGroups/AbPushout.v b/theories/Algebra/AbGroups/AbPushout.v
@@ -1,4 +1,4 @@
-Require Import Basics Types Truncations.Core.
+From HoTT Require Import Basics Types Truncations.Core.
 Require Import WildCat.Core HSet.
 Require Import Algebra.Groups.Group.
 Require Export Algebra.Groups.QuotientGroup.

diff --git a/theories/Algebra/AbGroups/AbelianGroup.v b/theories/Algebra/AbGroups/AbelianGroup.v
@@ -1,4 +1,4 @@
-Require Import Basics Types.
+From HoTT Require Import Basics Types.
 Require Import Spaces.Nat.Core Spaces.Int.
 Require Export Classes.interfaces.canonical_names (Zero, zero, Plus, plus, Negate, negate, Involutive, involutive).
 Require Export Classes.interfaces.abstract_algebra (IsAbGroup(..), abgroup_group, abgroup_commutative).

diff --git a/theories/Algebra/AbGroups/Abelianization.v b/theories/Algebra/AbGroups/Abelianization.v
@@ -1,4 +1,4 @@
-Require Import Basics Types Truncations.Core.
+From HoTT Require Import Basics Types Truncations.Core.
 Require Import Cubical.DPath WildCat.
 Require Import Colimits.Coeq.
 Require Import Algebra.AbGroups.AbelianGroup.

diff --git a/theories/Algebra/AbGroups/Biproduct.v b/theories/Algebra/AbGroups/Biproduct.v
@@ -1,4 +1,4 @@
-Require Import Basics Types Truncations.Core.
+From HoTT Require Import Basics Types Truncations.Core.
 Require Import WildCat.
 Require Import HSet.
 Require Import AbelianGroup.

diff --git a/theories/Algebra/AbGroups/Centralizer.v b/theories/Algebra/AbGroups/Centralizer.v
@@ -1,4 +1,4 @@
-Require Import Basics Types Truncations.Core.
+From HoTT Require Import Basics Types Truncations.Core.
 Require Import HFiber AbelianGroup.
 
 (* Given a group [G], we define the centralizer of an element [g : G] as a subgroup and use this to show that the cyclic subgroup generated by [g] is abelian. *)

diff --git a/theories/Algebra/AbGroups/Z.v b/theories/Algebra/AbGroups/Z.v
@@ -1,4 +1,4 @@
-Require Import Basics.
+From HoTT Require Import Basics.
 Require Import Spaces.Pos.Core Spaces.Int.
 Require Import Algebra.AbGroups.AbelianGroup.
 

diff --git a/theories/Algebra/AbSES/BaerSum.v b/theories/Algebra/AbSES/BaerSum.v
@@ -1,4 +1,4 @@
-Require Import Basics Types.
+From HoTT Require Import Basics Types.
 Require Import WildCat Pointed.Core.
 Require Import AbGroups.AbelianGroup AbGroups.Biproduct AbGroups.AbHom.
 Require Import AbSES.Core AbSES.Pullback AbSES.Pushout AbSES.DirectSum.

diff --git a/theories/Algebra/AbSES/Core.v b/theories/Algebra/AbSES/Core.v
@@ -1,4 +1,4 @@
-Require Import Basics Types Truncations.Core.
+From HoTT Require Import Basics Types Truncations.Core.
 Require Import HSet WildCat Pointed.
 Require Import Groups.QuotientGroup Groups.ShortExactSequence.
 Require Import AbelianGroup AbGroups.Biproduct AbHom.

diff --git a/theories/Algebra/AbSES/DirectSum.v b/theories/Algebra/AbSES/DirectSum.v
@@ -1,4 +1,4 @@
-Require Import Basics Types Truncations.Core.
+From HoTT Require Import Basics Types Truncations.Core.
 Require Import Pointed.Core.
 Require Import WildCat.Core Homotopy.ExactSequence.
 Require Import AbGroups.AbelianGroup AbSES.Core AbGroups.Biproduct.

diff --git a/theories/Algebra/AbSES/Ext.v b/theories/Algebra/AbSES/Ext.v
@@ -1,4 +1,4 @@
-Require Import Basics Types Truncations.Core.
+From HoTT Require Import Basics Types Truncations.Core.
 Require Import Pointed WildCat.
 Require Import Truncations.SeparatedTrunc.
 Require Import AbelianGroup AbHom AbProjective.

diff --git a/theories/Algebra/AbSES/Pullback.v b/theories/Algebra/AbSES/Pullback.v
@@ -1,4 +1,4 @@
-Require Import Basics Types.
+From HoTT Require Import Basics Types.
 Require Import HSet Limits.Pullback.
 Require Import WildCat Pointed.Core Homotopy.ExactSequence.
 Require Import Modalities.ReflectiveSubuniverse.

diff --git a/theories/Algebra/AbSES/PullbackFiberSequence.v b/theories/Algebra/AbSES/PullbackFiberSequence.v
@@ -1,4 +1,4 @@
-Require Import Basics Types HSet HFiber Limits.Pullback.
+From HoTT Require Import Basics Types HSet HFiber Limits.Pullback.
 Require Import WildCat Pointed.Core Homotopy.ExactSequence.
 Require Import Groups.QuotientGroup.
 Require Import AbGroups.AbelianGroup AbGroups.AbPullback AbGroups.Biproduct.

diff --git a/theories/Algebra/AbSES/Pushout.v b/theories/Algebra/AbSES/Pushout.v
@@ -1,4 +1,4 @@
-Require Import Basics Types Truncations.Core.
+From HoTT Require Import Basics Types Truncations.Core.
 Require Import WildCat Pointed.Core Homotopy.ExactSequence HIT.epi.
 Require Import Modalities.ReflectiveSubuniverse.
 Require Import AbelianGroup AbPushout AbHom AbGroups.Biproduct.

diff --git a/theories/Algebra/AbSES/SixTerm.v b/theories/Algebra/AbSES/SixTerm.v
@@ -1,4 +1,4 @@
-Require Import Basics Types WildCat HSet Pointed.Core Pointed.pTrunc Pointed.pEquiv
+From HoTT Require Import Basics Types WildCat HSet Pointed.Core Pointed.pTrunc Pointed.pEquiv
   Modalities.ReflectiveSubuniverse Truncations.Core Truncations.SeparatedTrunc
   AbGroups Homotopy.ExactSequence Spaces.Int Spaces.FreeInt
   AbSES.Core AbSES.Pullback AbSES.Pushout BaerSum Ext PullbackFiberSequence.

diff --git a/theories/Algebra/Aut.v b/theories/Algebra/Aut.v
@@ -1,4 +1,4 @@
-Require Import Basics.
+From HoTT Require Import Basics.
 Require Import Truncations.
 Require Import Algebra.ooGroup.
 Require Import Universes.BAut.

diff --git a/theories/Algebra/Groups/Finite.v b/theories/Algebra/Groups/Finite.v
@@ -1,4 +1,4 @@
-Require Import Basics Types.
+From HoTT Require Import Basics Types.
 Require Import Algebra.Groups.Group.
 Require Import Algebra.Groups.Subgroup.
 Require Import Algebra.Groups.QuotientGroup.

diff --git a/theories/Algebra/Groups/FreeGroup.v b/theories/Algebra/Groups/FreeGroup.v
@@ -1,4 +1,5 @@
-Require Import Basics Types Group Subgroup
+From HoTT Require Import Basics Types.
+Require Import Group Subgroup
   WildCat.Core WildCat.Universe Colimits.Coeq
   Truncations.Core Truncations.SeparatedTrunc
   Spaces.List.Core Spaces.List.Theory.

diff --git a/theories/Algebra/Groups/FreeProduct.v b/theories/Algebra/Groups/FreeProduct.v
@@ -1,4 +1,4 @@
-Require Import Basics Types.
+From HoTT Require Import Basics Types.
 Require Import WildCat.Core WildCat.Coproducts.
 Require Import Cubical.DPath.
 Require Import Spaces.List.Core Spaces.List.Theory.

diff --git a/theories/Algebra/Groups/Group.v b/theories/Algebra/Groups/Group.v
@@ -1,4 +1,4 @@
-Require Import Basics Types HProp HFiber HSet.
+From HoTT Require Import Basics Types HProp HFiber HSet.
 Require Import Homotopy.IdentitySystems.
 Require Import (notations) Classes.interfaces.canonical_names.
 Require Export (hints) Classes.interfaces.abstract_algebra.

diff --git a/theories/Algebra/Groups/GroupCoeq.v b/theories/Algebra/Groups/GroupCoeq.v
@@ -1,4 +1,4 @@
-Require Import Basics Types.
+From HoTT Require Import Basics Types.
 Require Import WildCat.Core.
 Require Import Truncations.Core.
 Require Import Algebra.Groups.Group.

diff --git a/theories/Algebra/Groups/GrpPullback.v b/theories/Algebra/Groups/GrpPullback.v
@@ -1,4 +1,4 @@
-Require Import Basics Types Limits.Pullback Cubical.PathSquare.
+From HoTT Require Import Basics Types Limits.Pullback Cubical.PathSquare.
 Require Import Algebra.Groups.Group.
 Require Import WildCat.Core.
 

diff --git a/theories/Algebra/Groups/Presentation.v b/theories/Algebra/Groups/Presentation.v
@@ -1,4 +1,4 @@
-Require Import Basics Types.
+From HoTT Require Import Basics Types.
 Require Import Truncations.Core.
 Require Import Algebra.Groups.Group.
 Require Import Algebra.Groups.FreeGroup.

diff --git a/theories/Algebra/Groups/QuotientGroup.v b/theories/Algebra/Groups/QuotientGroup.v
@@ -1,4 +1,4 @@
-Require Import Basics Types.
+From HoTT Require Import Basics Types.
 Require Import Truncations.Core.
 Require Import Algebra.Congruence.
 Require Import Algebra.Groups.Group.

diff --git a/theories/Algebra/Groups/ShortExactSequence.v b/theories/Algebra/Groups/ShortExactSequence.v
@@ -1,4 +1,4 @@
-Require Import Basics Types.
+From HoTT Require Import Basics Types.
 Require Import Truncations.Core.
 Require Import WildCat.Core Pointed.
 Require Import Groups.Group Groups.Subgroup.

diff --git a/theories/Algebra/Groups/Subgroup.v b/theories/Algebra/Groups/Subgroup.v
@@ -1,4 +1,4 @@
-Require Import Basics Types HFiber WildCat.Core WildCat.Equiv.
+From HoTT Require Import Basics Types HFiber WildCat.Core WildCat.Equiv.
 Require Import Truncations.Core Modalities.Modality.
 Require Export Modalities.Modality (conn_map_factor1_image).
 Require Import Algebra.Groups.Group Universes.TruncType Universes.HSet.

diff --git a/theories/Algebra/Rings/Ideal.v b/theories/Algebra/Rings/Ideal.v
@@ -1,4 +1,4 @@
-Require Import Basics Types.
+From HoTT Require Import Basics Types.
 Require Import Spaces.Finite.Fin.
 Require Import Classes.interfaces.canonical_names.
 Require Import Algebra.Rings.Ring.

diff --git a/theories/Algebra/ooAction.v b/theories/Algebra/ooAction.v
@@ -1,4 +1,4 @@
-Require Import Basics.
+From HoTT Require Import Basics.
 Require Import Algebra.ooGroup.
 
 Local Open Scope path_scope.

diff --git a/theories/Algebra/ooGroup.v b/theories/Algebra/ooGroup.v
@@ -1,4 +1,4 @@
-Require Import Basics Types.
+From HoTT Require Import Basics Types.
 Require Import Pointed.
 Require Import Truncations.Core Truncations.Connectedness.
 Require Import Homotopy.ClassifyingSpace.

diff --git a/theories/Analysis/Locator.v b/theories/Analysis/Locator.v
@@ -1,4 +1,4 @@
-Require Import
+From HoTT Require Import
   Basics DProp Misc.BoundedSearch Spaces.Finite.Fin ExcludedMiddle
   Classes.interfaces.abstract_algebra
   Classes.interfaces.orders

diff --git a/theories/Categories/Grothendieck/PseudofunctorToCat.v b/theories/Categories/Grothendieck/PseudofunctorToCat.v
@@ -6,7 +6,7 @@ Require Import Category.Morphisms Cat.Morphisms.
 Require Import Functor.Composition.Core.
 Require Import Functor.Identity.
 Require Import FunctorCategory.Core.
-Require Import Basics Types HoTT.Tactics.
+From HoTT Require Import Basics Types Tactics.
 
 Set Universe Polymorphism.
 Set Implicit Arguments.

diff --git a/theories/Categories/SimplicialSets.v b/theories/Categories/SimplicialSets.v
@@ -1,5 +1,5 @@
 (** * The simplex category Δ, and the precategory of simplicial sets, [Δᵒᵖ → set] *)
-Require Import Basics Types Spaces.Nat.Core.
+From HoTT Require Import Basics Types Spaces.Nat.Core.
 Require Import Category.Core Functor.Core Functor.Paths.
 Require Import SetCategory.Core.
 Require Import ChainCategory FunctorCategory.Core.

diff --git a/theories/Colimits/Coeq.v b/theories/Colimits/Coeq.v
@@ -1,4 +1,4 @@
-Require Import Basics.
+From HoTT Require Import Basics.
 Require Import Types.Paths Types.Arrow Types.Sigma Types.Forall Types.Universe Types.Prod.
 Require Import Colimits.GraphQuotient.
 Require Import Homotopy.IdentitySystems.

diff --git a/theories/Colimits/Colimit.v b/theories/Colimits/Colimit.v
@@ -1,4 +1,4 @@
-Require Import Basics Types.
+From HoTT Require Import Basics Types.
 Require Import Diagrams.Diagram.
 Require Import Diagrams.Graph.
 Require Import Diagrams.Cocone.

diff --git a/theories/Colimits/Colimit_Coequalizer.v b/theories/Colimits/Colimit_Coequalizer.v
@@ -1,4 +1,4 @@
-Require Import Basics.
+From HoTT Require Import Basics.
 Require Import Types.
 Require Import Diagrams.ParallelPair.
 Require Import Diagrams.Cocone.

diff --git a/theories/Colimits/Colimit_Flattening.v b/theories/Colimits/Colimit_Flattening.v
@@ -1,4 +1,4 @@
-Require Import Basics.
+From HoTT Require Import Basics.
 Require Import Types.
 Require Import Diagrams.Diagram.
 Require Import Diagrams.Graph.

diff --git a/theories/Colimits/Colimit_Prod.v b/theories/Colimits/Colimit_Prod.v
@@ -1,4 +1,4 @@
-Require Import Basics.
+From HoTT Require Import Basics.
 Require Import Types.
 Require Import Diagrams.Diagram.
 Require Import Colimits.Colimit.

diff --git a/theories/Colimits/Colimit_Pushout.v b/theories/Colimits/Colimit_Pushout.v
@@ -1,4 +1,4 @@
-Require Import Basics.
+From HoTT Require Import Basics.
 Require Import Types.
 Require Import Diagrams.Graph.
 Require Import Diagrams.Diagram.

diff --git a/theories/Colimits/Colimit_Pushout_Flattening.v b/theories/Colimits/Colimit_Pushout_Flattening.v
@@ -1,4 +1,4 @@
-Require Import Basics.
+From HoTT Require Import Basics.
 Require Import Types.
 Require Import Diagrams.Diagram.
 Require Import Diagrams.DDiagram.

diff --git a/theories/Colimits/Colimit_Sigma.v b/theories/Colimits/Colimit_Sigma.v
@@ -1,4 +1,4 @@
-Require Import Basics.
+From HoTT Require Import Basics.
 Require Import Types.
 Require Import Diagrams.Diagram.
 Require Import Diagrams.Graph.

diff --git a/theories/Colimits/Pushout.v b/theories/Colimits/Pushout.v
@@ -1,4 +1,4 @@
-Require Import Basics.
+From HoTT Require Import Basics.
 Require Import Types.Paths Types.Forall Types.Arrow Types.Sigma Types.Sum Types.Universe.
 Require Export Colimits.Coeq.
 Require Import Homotopy.IdentitySystems.

diff --git a/theories/Colimits/Quotient.v b/theories/Colimits/Quotient.v
@@ -1,4 +1,4 @@
-Require Import Basics.
+From HoTT Require Import Basics.
 Require Import Types.
 Require Import HSet.
 Require Import TruncType.

diff --git a/theories/Colimits/Sequential.v b/theories/Colimits/Sequential.v
@@ -2,7 +2,7 @@
 
 (** We present a proof of the conjecture that sequential colimits in HoTT appropriately commute with Σ-types. As a corollary, we characterize the path space of a sequential colimit as a sequential colimit of path spaces. For the written account of these results see https://www.cs.cornell.edu/~ks858/papers/sequential_colimits_homotopy.pdf. *)
 
-Require Import Basics.
+From HoTT Require Import Basics.
 Require Import Types.
 Require Import Diagrams.Diagram.
 Require Import Diagrams.Sequence.

diff --git a/theories/Cubical/DPath.v b/theories/Cubical/DPath.v
@@ -1,4 +1,4 @@
-Require Import Basics.
+From HoTT Require Import Basics.
 Require Import Types.Paths Types.Sigma Types.Forall.
 
 Declare Scope dpath_scope.

diff --git a/theories/Cubical/DPathCube.v b/theories/Cubical/DPathCube.v
@@ -1,4 +1,4 @@
-Require Import Basics.
+From HoTT Require Import Basics.
 Require Import Cubical.DPath.
 Require Import Cubical.PathSquare.
 Require Import Cubical.DPathSquare.

diff --git a/theories/Cubical/DPathSquare.v b/theories/Cubical/DPathSquare.v
@@ -1,4 +1,4 @@
-Require Import Basics.
+From HoTT Require Import Basics.
 Require Import Types.Paths.
 Require Import Cubical.DPath.
 Require Import Cubical.PathSquare.

diff --git a/theories/Cubical/PathCube.v b/theories/Cubical/PathCube.v
@@ -1,4 +1,4 @@
-Require Import Basics.
+From HoTT Require Import Basics.
 Require Import Cubical.DPath.
 Require Import Cubical.PathSquare.
 Require Import Cubical.DPathSquare.

diff --git a/theories/Cubical/PathSquare.v b/theories/Cubical/PathSquare.v
@@ -1,4 +1,4 @@
-Require Import Basics.
+From HoTT Require Import Basics.
 Require Import Types.Paths Types.Prod.
 Require Import DPath.
 

diff --git a/theories/Diagrams/Cocone.v b/theories/Diagrams/Cocone.v
@@ -1,4 +1,4 @@
-Require Import Basics.
+From HoTT Require Import Basics.
 Require Import Types.
 Require Import Diagrams.Graph.
 Require Import Diagrams.Diagram.

diff --git a/theories/Diagrams/Cone.v b/theories/Diagrams/Cone.v
@@ -1,4 +1,4 @@
-Require Import Basics.
+From HoTT Require Import Basics.
 Require Import Types.
 Require Import Diagrams.Graph.
 Require Import Diagrams.Diagram.

diff --git a/theories/Diagrams/ConstantDiagram.v b/theories/Diagrams/ConstantDiagram.v
@@ -1,4 +1,4 @@
-Require Import Basics Types.Paths.
+From HoTT Require Import Basics Types.Paths.
 Require Import Cone.
 Require Import Cocone.
 Require Import Diagram.

diff --git a/theories/Diagrams/DDiagram.v b/theories/Diagrams/DDiagram.v
@@ -1,4 +1,4 @@
-Require Import Basics.
+From HoTT Require Import Basics.
 Require Import Diagrams.Graph.
 Require Import Diagrams.Diagram.
 

diff --git a/theories/Diagrams/Diagram.v b/theories/Diagrams/Diagram.v
@@ -1,4 +1,4 @@
-Require Import Basics.
+From HoTT Require Import Basics.
 Require Import Types.
 Require Import HoTT.Tactics.
 Require Import Diagrams.CommutativeSquares.

diff --git a/theories/Diagrams/ParallelPair.v b/theories/Diagrams/ParallelPair.v
@@ -1,4 +1,4 @@
-Require Import Basics.
+From HoTT Require Import Basics.
 Require Import Types.
 Require Import Diagrams.Graph.
 Require Import Diagrams.Diagram.

diff --git a/theories/Diagrams/Sequence.v b/theories/Diagrams/Sequence.v
@@ -1,4 +1,4 @@
-Require Import Basics.
+From HoTT Require Import Basics.
 Require Import Diagrams.Graph.
 Require Import Diagrams.Diagram.
 

diff --git a/theories/Diagrams/Span.v b/theories/Diagrams/Span.v
@@ -1,4 +1,4 @@
-Require Import Basics.
+From HoTT Require Import Basics.
 Require Import Types.
 Require Import Diagrams.Graph.
 Require Import Diagrams.Diagram.

diff --git a/theories/Equiv/BiInv.v b/theories/Equiv/BiInv.v
@@ -1,4 +1,4 @@
-Require Import Basics Types.Prod Types.Equiv.
+From HoTT Require Import Basics Types.Prod Types.Equiv.
 
 Local Open Scope path_scope.
 Generalizable Variables A B f.

diff --git a/theories/HFiber.v b/theories/HFiber.v
@@ -1,4 +1,4 @@
-Require Import Basics Types Diagrams.CommutativeSquares HSet.
+From HoTT Require Import Basics Types Diagrams.CommutativeSquares HSet.
 
 Local Open Scope equiv_scope.
 Local Open Scope path_scope.

diff --git a/theories/HIT/epi.v b/theories/HIT/epi.v
@@ -1,4 +1,4 @@
-Require Import Basics.
+From HoTT Require Import Basics.
 Require Import Types.
 Require Import TruncType.
 Require Import ReflectiveSubuniverse.

diff --git a/theories/Homotopy/Bouquet.v b/theories/Homotopy/Bouquet.v
@@ -1,4 +1,4 @@
-Require Import Basics Types.
+From HoTT Require Import Basics Types.
 Require Import Pointed WildCat.
 Require Import Algebra.Groups.
 Require Import Modalities.ReflectiveSubuniverse Truncations.Core.

diff --git a/theories/Homotopy/ClassifyingSpace.v b/theories/Homotopy/ClassifyingSpace.v
@@ -1,4 +1,4 @@
-Require Import Basics Types.
+From HoTT Require Import Basics Types.
 Require Import Pointed WildCat.
 Require Import Cubical.DPath Cubical.PathSquare Cubical.DPathSquare.
 Require Import Algebra.AbGroups.

diff --git a/theories/Homotopy/Cover.v b/theories/Homotopy/Cover.v
@@ -1,4 +1,4 @@
-Require Import Basics Types HFiber Truncations.Core Truncations.SeparatedTrunc Pointed
+From HoTT Require Import Basics Types HFiber Truncations.Core Truncations.SeparatedTrunc Pointed
   Modalities.ReflectiveSubuniverse.
 
 Local Open Scope pointed_scope.

diff --git a/theories/Homotopy/EMSpace.v b/theories/Homotopy/EMSpace.v
@@ -1,4 +1,4 @@
-Require Import Basics Types.
+From HoTT Require Import Basics Types.
 Require Import Pointed.
 Require Import Cubical.DPath.
 Require Import Algebra.AbGroups.