From 4ecd34370a3cfafb289e8fa5136a559695a3f990 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Tue, 8 Oct 2024 02:47:59 +0100 Subject: [PATCH 1/2] chore: remove Cubical.v indexing file We remove the Cubical.v indexing file since we always wish to have finer dependencies when using the Cubical library. This allows us to refine some imports elsewhere. Signed-off-by: Ali Caglayan --- theories/Algebra/AbGroups/Abelianization.v | 2 +- theories/Algebra/Groups/FreeProduct.v | 2 +- theories/Cubical.v | 5 ----- theories/HoTT.v | 8 +++++++- theories/Homotopy/CayleyDickson.v | 2 +- theories/Homotopy/ClassifyingSpace.v | 3 ++- theories/Homotopy/HSpaceS1.v | 2 +- theories/Homotopy/Join/Core.v | 3 ++- theories/Homotopy/Suspension.v | 2 +- theories/Spaces/Torus/Torus.v | 4 ++-- theories/Spaces/Torus/TorusEquivCircles.v | 3 ++- 11 files changed, 20 insertions(+), 16 deletions(-) delete mode 100644 theories/Cubical.v diff --git a/theories/Algebra/AbGroups/Abelianization.v b/theories/Algebra/AbGroups/Abelianization.v index 4b45f9891d5..ff8e35bf5b2 100644 --- a/theories/Algebra/AbGroups/Abelianization.v +++ b/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. diff --git a/theories/Algebra/Groups/FreeProduct.v b/theories/Algebra/Groups/FreeProduct.v index ce8667ba763..e4459613b60 100644 --- a/theories/Algebra/Groups/FreeProduct.v +++ b/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. diff --git a/theories/Cubical.v b/theories/Cubical.v deleted file mode 100644 index cd1c6d2a455..00000000000 --- a/theories/Cubical.v +++ /dev/null @@ -1,5 +0,0 @@ -Require Export Cubical.DPath. -Require Export Cubical.PathSquare. -Require Export Cubical.DPathSquare. -Require Export Cubical.PathCube. -Require Export Cubical.DPathCube. \ No newline at end of file diff --git a/theories/HoTT.v b/theories/HoTT.v index cce25a4b42e..d41ff49c6cd 100644 --- a/theories/HoTT.v +++ b/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. diff --git a/theories/Homotopy/CayleyDickson.v b/theories/Homotopy/CayleyDickson.v index 9bae2ba3106..619c70b2a94 100644 --- a/theories/Homotopy/CayleyDickson.v +++ b/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. diff --git a/theories/Homotopy/ClassifyingSpace.v b/theories/Homotopy/ClassifyingSpace.v index 7fdf896df43..e7f1edab43c 100644 --- a/theories/Homotopy/ClassifyingSpace.v +++ b/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. diff --git a/theories/Homotopy/HSpaceS1.v b/theories/Homotopy/HSpaceS1.v index d4d8b9f7d95..2698abf8daf 100644 --- a/theories/Homotopy/HSpaceS1.v +++ b/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. diff --git a/theories/Homotopy/Join/Core.v b/theories/Homotopy/Join/Core.v index c6c480aa472..5c1c5178585 100644 --- a/theories/Homotopy/Join/Core.v +++ b/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. diff --git a/theories/Homotopy/Suspension.v b/theories/Homotopy/Suspension.v index ff0c308f4c6..10e6baf66dd 100644 --- a/theories/Homotopy/Suspension.v +++ b/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. diff --git a/theories/Spaces/Torus/Torus.v b/theories/Spaces/Torus/Torus.v index 4bbc2a5e9fb..9fb49b192c3 100644 --- a/theories/Spaces/Torus/Torus.v +++ b/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. *) diff --git a/theories/Spaces/Torus/TorusEquivCircles.v b/theories/Spaces/Torus/TorusEquivCircles.v index eed92e15b92..9b5adeba95b 100644 --- a/theories/Spaces/Torus/TorusEquivCircles.v +++ b/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. *) From 75369bb239f62c930f2a749a994437911290c18b Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Tue, 8 Oct 2024 03:04:33 +0100 Subject: [PATCH 2/2] fix tests Signed-off-by: Ali Caglayan --- test/bugs/github1758.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/bugs/github1758.v b/test/bugs/github1758.v index ac341eb1a6f..699e1a64c99 100644 --- a/test/bugs/github1758.v +++ b/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. *)