Merge pull request #2111 from Alizter/ps/rr/chore__remove_cubical_v_i…

…ndexing_file

chore: remove Cubical.v indexing file

test/bugs/github1758.v

@@ -1,5 +1,5 @@
 From HoTT Require Import Basics.Overture HIT.Interval HIT.Flattening Colimits.GraphQuotient
-          Spaces.Torus.Torus Cubical.
+          Spaces.Torus.Torus Cubical.DPath.
 
 (* Test that various higher inductive types are defined correctly.  If they are defined in the most naive way, two uses of the induction principle that are definitionally equal on the point constructors will be considered definitionally equal, which is inconsistent.  There is an idiom that must be used in order to force Coq to regard the supplementary data as being required as well.  See, for example, Colimits/GraphQuotient.v for the idiom. *)
 

theories/Algebra/AbGroups/Abelianization.v

@@ -1,5 +1,5 @@
 Require Import Basics Types Truncations.Core.
-Require Import Cubical WildCat.
+Require Import Cubical.DPath WildCat.
 Require Import Colimits.Coeq.
 Require Import Algebra.AbGroups.AbelianGroup.
 Require Import Modalities.ReflectiveSubuniverse.

theories/Algebra/Groups/FreeProduct.v

@@ -1,5 +1,5 @@
 Require Import Basics Types.
-Require Import Cubical.
+Require Import Cubical.DPath.
 Require Import Spaces.List.Core Spaces.List.Theory.
 Require Import Colimits.Pushout.
 Require Import Truncations.Core Truncations.SeparatedTrunc.

theories/HoTT.v

@@ -6,7 +6,13 @@
 Require Export HoTT.Basics.
 Require Export HoTT.Types.
 Require Export HoTT.WildCat.
-Require Export HoTT.Cubical.
+
+Require Export HoTT.Cubical.DPath.
+Require Export HoTT.Cubical.PathSquare.
+Require Export HoTT.Cubical.DPathSquare.
+Require Export HoTT.Cubical.PathCube.
+Require Export HoTT.Cubical.DPathCube.
+
 Require Export HoTT.Pointed.
 Require Export HoTT.Truncations.
 

theories/Homotopy/CayleyDickson.v

@@ -1,5 +1,5 @@
 Require Import Classes.interfaces.abstract_algebra.
-Require Import Cubical.
+Require Import Cubical.DPath Cubical.PathSquare.
 Require Import Pointed.Core Pointed.pSusp.
 Require Import Homotopy.HSpace.Core.
 Require Import Homotopy.Suspension.

theories/Homotopy/ClassifyingSpace.v

@@ -1,5 +1,6 @@
 Require Import Basics Types.
-Require Import Pointed Cubical WildCat.
+Require Import Pointed WildCat.
+Require Import Cubical.DPath Cubical.PathSquare Cubical.DPathSquare.
 Require Import Algebra.AbGroups.
 Require Import Homotopy.HSpace.Core.
 Require Import TruncType.

theories/Homotopy/HSpaceS1.v

@@ -1,5 +1,5 @@
 Require Import Classes.interfaces.canonical_names.
-Require Import Cubical.
+Require Import Cubical.DPath Cubical.PathSquare.
 Require Import Homotopy.Suspension.
 Require Import Homotopy.HSpace.Core.
 Require Import Homotopy.HSpace.Coherent.

theories/Homotopy/Join/Core.v

@@ -1,4 +1,5 @@
-Require Import Basics Types Cubical.
+Require Import Basics Types.
+Require Import Cubical.DPath Cubical.PathSquare.
 Require Import NullHomotopy.
 Require Import Extensions.
 Require Import Colimits.Pushout.

theories/Homotopy/Suspension.v

@@ -1,6 +1,6 @@
 Require Import Basics.
 Require Import Types.
-Require Import Cubical.
+Require Import Cubical.DPath Cubical.DPathSquare.
 Require Import WildCat.
 Require Import Colimits.Pushout.
 Require Import NullHomotopy.

theories/Spaces/Torus/Torus.v

@@ -1,5 +1,5 @@
-Require Import Basics.
-Require Import Cubical.
+Require Import Basics.Overture Basics.Equivalences Cubical.DPath
+  Cubical.PathSquare Cubical.DPathSquare Cubical.PathCube Cubical.DPathCube.
 
 (** In this file we define the Torus as a HIT generated by two loops and a square between them. *)
 

theories/Spaces/Torus/TorusEquivCircles.v

@@ -1,5 +1,6 @@
 Require Import Basics Types.
-Require Import Cubical.
+Require Import Cubical.DPath Cubical.PathSquare Cubical.DPathSquare
+  Cubical.PathCube Cubical.DPathCube.
 Require Import Spaces.Circle Spaces.Torus.Torus.
 
 (** In this file we prove that the torus is equivalent to the product of two circles. *)