Move Rationals around

agda · Jul 18, 2023 · 2a510bc · 2a510bc
1 parent b56db83
commit 2a510bc
Show file tree

Hide file tree

Showing 14 changed files with 33 additions and 33 deletions.
diff --git a/Cubical/Algebra/CommRing/Instances/QuoQ.agda → ...Algebra/CommRing/Instances/Rationals.agda b/Cubical/Algebra/CommRing/Instances/QuoQ.agda → ...Algebra/CommRing/Instances/Rationals.agda
@@ -4,12 +4,12 @@
 
 -}
 {-# OPTIONS --safe #-}
-module Cubical.Algebra.CommRing.Instances.QuoQ where
+module Cubical.Algebra.CommRing.Instances.Rationals where
 
 open import Cubical.Foundations.Prelude
 
 open import Cubical.Algebra.CommRing
-open import Cubical.HITs.Rationals.QuoQ
+open import Cubical.Data.Rationals
   renaming (ℚ to ℚType ; _+_ to _+ℚ_; _·_ to _·ℚ_; -_ to -ℚ_)
 
 open CommRingStr

diff --git a/Cubical/Algebra/Field/Instances/QuoQ.agda → ...al/Algebra/Field/Instances/Rationals.agda b/Cubical/Algebra/Field/Instances/QuoQ.agda → ...al/Algebra/Field/Instances/Rationals.agda
@@ -4,7 +4,7 @@
 
 -}
 {-# OPTIONS --safe #-}
-module Cubical.Algebra.Field.Instances.QuoQ where
+module Cubical.Algebra.Field.Instances.Rationals where
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.HLevels
@@ -19,14 +19,14 @@ open import Cubical.Data.Int.MoreInts.QuoInt
            ; ·-zeroˡ to ·ℤ-zeroˡ
            ; ·-identityʳ to ·ℤ-identityʳ)
 open import Cubical.HITs.SetQuotients as SetQuot
-open import Cubical.HITs.Rationals.QuoQ
+open import Cubical.Data.Rationals
   using    (ℚ ; ℕ₊₁→ℤ ; isEquivRel∼)
 
 open import Cubical.Algebra.Field
 open import Cubical.Algebra.CommRing
 open import Cubical.Tactics.CommRingSolver.Reflection
 open import Cubical.Algebra.CommRing.Instances.QuoInt
-open import Cubical.Algebra.CommRing.Instances.QuoQ
+open import Cubical.Algebra.CommRing.Instances.Rationals
 
 open import Cubical.Relation.Nullary
 

diff --git a/Cubical/Data/Rationals.agda b/Cubical/Data/Rationals.agda
@@ -0,0 +1,7 @@
+-- This is the preferred version of the rationals in the library. Other
+-- versions can be found in the MoreRationals directory.
+{-# OPTIONS --safe #-}
+module Cubical.Data.Rationals where
+
+open import Cubical.Data.Rationals.Base public
+open import Cubical.Data.Rationals.Properties public
diff --git a/Cubical/HITs/Rationals/QuoQ/Base.agda → Cubical/Data/Rationals/Base.agda b/Cubical/HITs/Rationals/QuoQ/Base.agda → Cubical/Data/Rationals/Base.agda
@@ -1,5 +1,5 @@
 {-# OPTIONS --safe #-}
-module Cubical.HITs.Rationals.QuoQ.Base where
+module Cubical.Data.Rationals.Base where
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Equiv

diff --git a/Cubical/Data/Rationals/MoreRationals/HITQ.agda b/Cubical/Data/Rationals/MoreRationals/HITQ.agda
@@ -0,0 +1,4 @@
+{-# OPTIONS --safe #-}
+module Cubical.Data.Rationals.MoreRationals.HITQ where
+
+open import Cubical.Data.Rationals.MoreRationals.HITQ.Base public
diff --git a/Cubical/HITs/Rationals/HITQ/Base.agda → ...ta/Rationals/MoreRationals/HITQ/Base.agda b/Cubical/HITs/Rationals/HITQ/Base.agda → ...ta/Rationals/MoreRationals/HITQ/Base.agda
@@ -1,5 +1,5 @@
 {-# OPTIONS --safe #-}
-module Cubical.HITs.Rationals.HITQ.Base where
+module Cubical.Data.Rationals.MoreRationals.HITQ.Base where
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.HLevels

diff --git a/Cubical/Data/Rationals/MoreRationals/SigmaQ.agda b/Cubical/Data/Rationals/MoreRationals/SigmaQ.agda
@@ -0,0 +1,6 @@
+{-# OPTIONS --safe #-}
+module Cubical.Data.Rationals.MoreRationals.SigmaQ where
+
+open import Cubical.Data.Rationals.MoreRationals.SigmaQ.Base public
+
+open import Cubical.Data.Rationals.MoreRationals.SigmaQ.Properties public
diff --git a/Cubical/HITs/Rationals/SigmaQ/Base.agda → .../Rationals/MoreRationals/SigmaQ/Base.agda b/Cubical/HITs/Rationals/SigmaQ/Base.agda → .../Rationals/MoreRationals/SigmaQ/Base.agda
@@ -1,5 +1,5 @@
 {-# OPTIONS --safe #-}
-module Cubical.HITs.Rationals.SigmaQ.Base where
+module Cubical.Data.Rationals.MoreRationals.SigmaQ.Base where
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.HLevels

diff --git a/...cal/HITs/Rationals/SigmaQ/Properties.agda → ...nals/MoreRationals/SigmaQ/Properties.agda b/...cal/HITs/Rationals/SigmaQ/Properties.agda → ...nals/MoreRationals/SigmaQ/Properties.agda
@@ -1,5 +1,5 @@
 {-# OPTIONS --safe #-}
-module Cubical.HITs.Rationals.SigmaQ.Properties where
+module Cubical.Data.Rationals.MoreRationals.SigmaQ.Properties where
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Function
@@ -17,8 +17,8 @@ open import Cubical.Data.Sigma
 open import Cubical.Data.Nat.GCD
 open import Cubical.Data.Nat.Coprime
 
-open import Cubical.HITs.Rationals.QuoQ as Quo using (ℕ₊₁→ℤ)
-import Cubical.HITs.Rationals.SigmaQ.Base as Sigma
+open import Cubical.Data.Rationals as Quo using (ℕ₊₁→ℤ)
+import Cubical.Data.Rationals.MoreRationals.SigmaQ.Base as Sigma
 
 
 reduce : Quo.ℚ → Sigma.ℚ

diff --git a/Cubical/HITs/Rationals/QuoQ/Properties.agda → Cubical/Data/Rationals/Properties.agda b/Cubical/HITs/Rationals/QuoQ/Properties.agda → Cubical/Data/Rationals/Properties.agda
@@ -1,5 +1,5 @@
 {-# OPTIONS --safe #-}
-module Cubical.HITs.Rationals.QuoQ.Properties where
+module Cubical.Data.Rationals.Properties where
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Isomorphism
@@ -17,7 +17,7 @@ open import Cubical.Data.Sigma
 open import Cubical.Data.Sum
 open import Cubical.Relation.Nullary
 
-open import Cubical.HITs.Rationals.QuoQ.Base
+open import Cubical.Data.Rationals.Base
 
 ℚ-cancelˡ : ∀ {a b} (c : ℕ₊₁) → [ ℕ₊₁→ℤ c ℤ.· a / c ·₊₁ b ] ≡ [ a / b ]
 ℚ-cancelˡ {a} {b} c = eq/ _ _

diff --git a/Cubical/HITs/Rationals/HITQ.agda b/Cubical/HITs/Rationals/HITQ.agda
diff --git a/Cubical/HITs/Rationals/QuoQ.agda b/Cubical/HITs/Rationals/QuoQ.agda
diff --git a/Cubical/HITs/Rationals/SigmaQ.agda b/Cubical/HITs/Rationals/SigmaQ.agda
diff --git a/Cubical/Papers/RepresentationIndependence.agda b/Cubical/Papers/RepresentationIndependence.agda
@@ -26,8 +26,9 @@ import Cubical.Data.Sigma.Properties           as Sigma
 import Cubical.HITs.PropositionalTruncation    as PropositionalTruncation
 import Cubical.HITs.Cost.Base                  as CostMonad
 import Cubical.HITs.SetQuotients               as SetQuotients
-import Cubical.HITs.Rationals.QuoQ             as SetQuoQ
-import Cubical.HITs.Rationals.SigmaQ           as SigmaQ
+import Cubical.Data.Rationals                  as SetQuoQ
+import Cubical.Data.Rationals.MoreRationals.SigmaQ
+                                               as SigmaQ
 -- 3.1
 import Cubical.Foundations.SIP                 as SIP
 import Cubical.Structures.Axioms               as Axioms