Merge remote-tracking branch 'origin/release-for-2.6.4.1' into fwelle…

…n/release-for-2.6.4.1

.gitignore

@@ -6,4 +6,3 @@ Cubical/*/Everything.agda
 !Cubical/Core/Everything.agda
 !Cubical/Foundations/Everything.agda
 !Cubical/Codata/Everything.agda
-!Cubical/Experiments/Everything.agda

CITATION.cff

@@ -3,6 +3,6 @@ message: "If you use this software, please cite it as below."
 authors:
 - name: "The Agda Community"
 title: "Cubical Agda Library"
-version: 0.6
-date-released: 2023-10-24
+version: 0.7
+date-released: 2024-01-22
 url: "https://github.com/agda/cubical"

Cubical/Algebra/AbGroup/Base.agda

@@ -315,10 +315,6 @@ module _ {ℓ ℓ' : Level} (AGr : Group ℓ) (BGr : AbGroup ℓ') where
       renaming (_·_ to _∙A_ ; inv to -A_
                 ; 1g to 1A ; ·IdR to ·IdRA)
 
-  trivGroupHom : GroupHom AGr (BGr *)
-  fst trivGroupHom x = 0B
-  snd trivGroupHom = makeIsGroupHom λ _ _ → sym (+IdRB 0B)
-
   compHom : GroupHom AGr (BGr *) → GroupHom AGr (BGr *) → GroupHom AGr (BGr *)
   fst (compHom f g) x = fst f x +B fst g x
   snd (compHom f g) =

Cubical/Algebra/AbGroup/Instances/DirectProduct.agda

@@ -0,0 +1,15 @@
+{-# OPTIONS --safe #-}
+module Cubical.Algebra.AbGroup.Instances.DirectProduct where
+
+open import Cubical.Data.Sigma
+open import Cubical.Algebra.AbGroup.Base
+open import Cubical.Algebra.Group.DirProd
+
+AbDirProd : ∀ {ℓ ℓ'} → AbGroup ℓ → AbGroup ℓ' → AbGroup (ℓ-max ℓ ℓ')
+AbDirProd G H =
+  Group→AbGroup (DirProd (AbGroup→Group G) (AbGroup→Group H)) comm
+  where
+  comm : (x y : fst G × fst H) → _ ≡ _
+  comm (g1 , h1) (g2 , h2) =
+    ΣPathP (AbGroupStr.+Comm (snd G) g1 g2
+          , AbGroupStr.+Comm (snd H) h1 h2)

Cubical/Algebra/AbGroup/Instances/Int.agda

@@ -0,0 +1,11 @@
+{-# OPTIONS --safe #-}
+module Cubical.Algebra.AbGroup.Instances.Int where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Data.Int
+open import Cubical.Algebra.AbGroup.Base
+open import Cubical.Algebra.Group.Base
+open import Cubical.Algebra.Group.Instances.Int
+
+ℤAbGroup : AbGroup ℓ-zero
+ℤAbGroup = Group→AbGroup ℤGroup +Comm

Cubical/Algebra/AbGroup/Instances/IntMod.agda

@@ -0,0 +1,89 @@
+{-# OPTIONS --safe #-}
+module Cubical.Algebra.AbGroup.Instances.IntMod where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Function
+
+open import Cubical.Algebra.AbGroup
+
+open import Cubical.Algebra.Group.Instances.Int
+open import Cubical.Algebra.AbGroup.Instances.Int
+open import Cubical.Algebra.Group.Instances.IntMod
+open import Cubical.Algebra.Group.Base
+open import Cubical.Algebra.Group.MorphismProperties
+open import Cubical.Algebra.Group.ZAction
+
+open import Cubical.Data.Empty as ⊥
+open import Cubical.Data.Nat renaming (_+_ to _+ℕ_ ; _·_ to _·ℕ_)
+open import Cubical.Data.Nat.Order
+open import Cubical.Data.Int
+  renaming (_+_ to _+ℤ_ ; _·_ to _·ℤ_ ; -_ to -ℤ_)
+open import Cubical.Data.Fin
+open import Cubical.Data.Fin.Arithmetic
+open import Cubical.Data.Sigma
+
+open import Cubical.HITs.SetQuotients as SQ
+open import Cubical.HITs.PropositionalTruncation as PT
+
+ℤAbGroup/_ : ℕ → AbGroup ℓ-zero
+ℤAbGroup/ n = Group→AbGroup (ℤGroup/ n) (comm n)
+  where
+  comm : (n : ℕ) (x y : fst (ℤGroup/ n))
+   → GroupStr._·_ (snd (ℤGroup/ n)) x y
+    ≡ GroupStr._·_ (snd (ℤGroup/ n)) y x
+  comm zero = +Comm
+  comm (suc n) = +ₘ-comm
+
+ℤ/2 : AbGroup ℓ-zero
+ℤ/2 = ℤAbGroup/ 2
+
+ℤ/2[2]≅ℤ/2 : AbGroupIso (ℤ/2 [ 2 ]ₜ) ℤ/2
+Iso.fun (fst ℤ/2[2]≅ℤ/2) = fst
+Iso.inv (fst ℤ/2[2]≅ℤ/2) x = x , cong (x +ₘ_) (+ₘ-rUnit x) ∙ x+x x
+  where
+  x+x : (x : ℤ/2 .fst) → x +ₘ x ≡ fzero
+  x+x = ℤ/2-elim refl refl
+Iso.rightInv (fst ℤ/2[2]≅ℤ/2) x = Σ≡Prop (λ _ → isProp≤) refl
+Iso.leftInv (fst ℤ/2[2]≅ℤ/2) x = Σ≡Prop (λ _ → isSetFin _ _) refl
+snd ℤ/2[2]≅ℤ/2 = makeIsGroupHom λ _ _ → refl
+
+ℤ/2/2≅ℤ/2 : AbGroupIso (ℤ/2 /^ 2) ℤ/2
+Iso.fun (fst ℤ/2/2≅ℤ/2) =
+  SQ.rec isSetFin (λ x → x) lem
+  where
+  lem : _
+  lem = ℤ/2-elim (ℤ/2-elim (λ _ → refl)
+        (PT.rec (isSetFin  _ _)
+          (uncurry (ℤ/2-elim
+          (λ p → ⊥.rec (snotz (sym (cong fst p))))
+           λ p → ⊥.rec (snotz (sym (cong fst p)))))))
+        (ℤ/2-elim (PT.rec (isSetFin  _ _)
+          (uncurry (ℤ/2-elim
+          (λ p → ⊥.rec (snotz (sym (cong fst p))))
+           λ p → ⊥.rec (snotz (sym (cong fst p))))))
+          λ _ → refl)
+Iso.inv (fst ℤ/2/2≅ℤ/2) = [_]
+Iso.rightInv (fst ℤ/2/2≅ℤ/2) _ = refl
+Iso.leftInv (fst ℤ/2/2≅ℤ/2) =
+  SQ.elimProp (λ _ → squash/ _ _) λ _ → refl
+snd ℤ/2/2≅ℤ/2 = makeIsGroupHom
+  (SQ.elimProp (λ _ → isPropΠ λ _ → isSetFin _ _)
+  λ a → SQ.elimProp (λ _ → isSetFin _ _) λ b → refl)
+
+ℤTorsion : (n : ℕ) → isContr (fst (ℤAbGroup [ (suc n) ]ₜ))
+fst (ℤTorsion n) = AbGroupStr.0g (snd (ℤAbGroup [ (suc n) ]ₜ))
+snd (ℤTorsion n) (a , p) = Σ≡Prop (λ _ → isSetℤ _ _)
+  (sym (help a (ℤ·≡· (pos (suc n)) a ∙ p)))
+  where
+  help : (a : ℤ) → a +ℤ pos n ·ℤ a ≡ 0 → a ≡ 0
+  help (pos zero) p = refl
+  help (pos (suc a)) p =
+    ⊥.rec (snotz (injPos (pos+ (suc a) (n ·ℕ suc a)
+                 ∙ cong (pos (suc a) +ℤ_) (pos·pos n (suc a)) ∙ p)))
+  help (negsuc a) p = ⊥.rec
+    (snotz (injPos (cong -ℤ_ (negsuc+ a (n ·ℕ suc a)
+                 ∙ (cong (negsuc a +ℤ_)
+                     (cong (-ℤ_) (pos·pos n (suc a)))
+                 ∙ sym (cong (negsuc a +ℤ_) (pos·negsuc n a)) ∙ p)))))

Cubical/Algebra/AbGroup/Instances/Pi.agda

@@ -0,0 +1,12 @@
+{-# OPTIONS --safe #-}
+module Cubical.Algebra.AbGroup.Instances.Pi where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+open import Cubical.Algebra.AbGroup
+open import Cubical.Algebra.Group.Instances.Pi
+
+module _ {ℓ ℓ' : Level} {X : Type ℓ} (G : X → AbGroup ℓ') where
+  ΠAbGroup : AbGroup (ℓ-max ℓ ℓ')
+  ΠAbGroup = Group→AbGroup (ΠGroup (λ x → AbGroup→Group (G x)))
+              λ f g i x → IsAbGroup.+Comm (AbGroupStr.isAbGroup (G x .snd)) (f x) (g x) i

Cubical/Algebra/AbGroup/Properties.agda

@@ -5,6 +5,17 @@ open import Cubical.Foundations.Prelude
 
 open import Cubical.Algebra.AbGroup.Base
 open import Cubical.Algebra.Group
+open import Cubical.Algebra.Group.Morphisms
+open import Cubical.Algebra.Group.MorphismProperties
+open import Cubical.Algebra.Group.QuotientGroup
+open import Cubical.Algebra.Group.Subgroup
+open import Cubical.Algebra.Group.ZAction
+
+open import Cubical.HITs.SetQuotients as SQ hiding (_/_)
+
+open import Cubical.Data.Int using (ℤ ; pos ; negsuc)
+open import Cubical.Data.Nat hiding (_+_)
+open import Cubical.Data.Sigma
 
 private variable
   ℓ : Level
@@ -24,3 +35,86 @@ module AbGroupTheory (A : AbGroup ℓ) where
 
   implicitInverse : ∀ {a b} → a + b ≡ 0g → b ≡ - a
   implicitInverse b+a≡0 = invUniqueR b+a≡0
+
+addGroupHom : (A B : AbGroup ℓ) (ϕ ψ : AbGroupHom A B) → AbGroupHom A B
+fst (addGroupHom A B ϕ ψ) x = AbGroupStr._+_ (snd B) (ϕ .fst x) (ψ .fst x)
+snd (addGroupHom A B ϕ ψ) = makeIsGroupHom
+  λ x y → cong₂ (AbGroupStr._+_ (snd B))
+                 (IsGroupHom.pres· (snd ϕ) x y)
+                 (IsGroupHom.pres· (snd ψ) x y)
+        ∙ AbGroupTheory.comm-4 B (fst ϕ x) (fst ϕ y) (fst ψ x) (fst ψ y)
+
+negGroupHom : (A B : AbGroup ℓ) (ϕ : AbGroupHom A B) → AbGroupHom A B
+fst (negGroupHom A B ϕ) x = AbGroupStr.-_ (snd B) (ϕ .fst x)
+snd (negGroupHom A B ϕ) =
+  makeIsGroupHom λ x y
+    → sym (IsGroupHom.presinv (snd ϕ) (AbGroupStr._+_ (snd A) x y))
+     ∙ cong (fst ϕ) (GroupTheory.invDistr (AbGroup→Group A) x y
+                  ∙ AbGroupStr.+Comm (snd A) _ _)
+     ∙ IsGroupHom.pres· (snd ϕ) _ _
+     ∙ cong₂ (AbGroupStr._+_ (snd B))
+             (IsGroupHom.presinv (snd ϕ) x)
+             (IsGroupHom.presinv (snd ϕ) y)
+
+subtrGroupHom : (A B : AbGroup ℓ) (ϕ ψ : AbGroupHom A B) → AbGroupHom A B
+subtrGroupHom A B ϕ ψ = addGroupHom A B ϕ (negGroupHom A B ψ)
+
+
+
+-- ℤ-multiplication defines a homomorphism for abelian groups
+private module _ (G : AbGroup ℓ) where
+  ℤ·isHom-pos : (n : ℕ) (x y : fst G)
+    → (pos n ℤ[ (AbGroup→Group G) ]· (AbGroupStr._+_ (snd G) x y))
+     ≡ AbGroupStr._+_ (snd G) ((pos n) ℤ[ (AbGroup→Group G) ]· x)
+                              ((pos n) ℤ[ (AbGroup→Group G) ]· y)
+  ℤ·isHom-pos zero x y =
+    sym (AbGroupStr.+IdR (snd G) (AbGroupStr.0g (snd G)))
+  ℤ·isHom-pos (suc n) x y =
+    cong₂ (AbGroupStr._+_ (snd G))
+          refl
+          (ℤ·isHom-pos n x y)
+    ∙ AbGroupTheory.comm-4 G _ _ _ _
+
+  ℤ·isHom-neg : (n : ℕ) (x y : fst G)
+    → (negsuc n ℤ[ (AbGroup→Group G) ]· (AbGroupStr._+_ (snd G) x y))
+     ≡ AbGroupStr._+_ (snd G) ((negsuc n) ℤ[ (AbGroup→Group G) ]· x)
+                              ((negsuc n) ℤ[ (AbGroup→Group G) ]· y)
+  ℤ·isHom-neg zero x y =
+    GroupTheory.invDistr (AbGroup→Group G) _ _
+    ∙ AbGroupStr.+Comm (snd G) _ _
+  ℤ·isHom-neg (suc n) x y =
+    cong₂ (AbGroupStr._+_ (snd G))
+          (GroupTheory.invDistr (AbGroup→Group G) _ _
+            ∙ AbGroupStr.+Comm (snd G) _ _)
+          (ℤ·isHom-neg n x y)
+    ∙ AbGroupTheory.comm-4 G _ _ _ _
+
+ℤ·isHom : (n : ℤ) (G : AbGroup ℓ) (x y : fst G)
+  → (n ℤ[ (AbGroup→Group G) ]· (AbGroupStr._+_ (snd G) x y))
+   ≡ AbGroupStr._+_ (snd G) (n ℤ[ (AbGroup→Group G) ]· x)
+                            (n ℤ[ (AbGroup→Group G) ]· y)
+ℤ·isHom (pos n) G = ℤ·isHom-pos G n
+ℤ·isHom (negsuc n) G = ℤ·isHom-neg G n
+
+-- left multiplication as a group homomorphism
+multₗHom : (G : AbGroup ℓ) (n : ℤ) → AbGroupHom G G
+fst (multₗHom G n) g = n ℤ[ (AbGroup→Group G) ]· g
+snd (multₗHom G n) = makeIsGroupHom (ℤ·isHom n G)
+
+-- Abelian groups quotiented by a natural number
+_/^_ : (G : AbGroup ℓ) (n : ℕ) → AbGroup ℓ
+G /^ n =
+  Group→AbGroup
+    ((AbGroup→Group G)
+     / (imSubgroup (multₗHom G (pos n))
+      , isNormalIm (multₗHom G (pos n)) (AbGroupStr.+Comm (snd G))))
+   (SQ.elimProp2 (λ _ _ → squash/ _ _)
+     λ a b → cong [_] (AbGroupStr.+Comm (snd G) a b))
+
+-- Torsion subgrous
+_[_]ₜ : (G : AbGroup ℓ) (n : ℕ) → AbGroup ℓ
+G [ n ]ₜ =
+  Group→AbGroup (Subgroup→Group (AbGroup→Group G)
+    (kerSubgroup (multₗHom G (pos n))))
+    λ {(x , p) (y , q) → Σ≡Prop (λ _ → isPropIsInKer (multₗHom G (pos n)) _)
+      (AbGroupStr.+Comm (snd G) _ _)}

Cubical/Algebra/CommAlgebra/Instances/Unit.agda

@@ -12,7 +12,7 @@ open import Cubical.Algebra.CommRing
 open import Cubical.Algebra.CommAlgebra.Base
 open import Cubical.Algebra.CommRing.Instances.Unit
 open import Cubical.Algebra.Algebra.Base using (IsAlgebraHom)
-open import Cubical.Tactics.CommRingSolver.Reflection
+open import Cubical.Tactics.CommRingSolver
 
 private
   variable
@@ -49,16 +49,11 @@ module _ (R : CommRing ℓ) where
 
       1≡0→isContr : isContr ⟨ A ⟩
       1≡0→isContr = 0a , λ a →
-        0a      ≡⟨ step1 a ⟩
+        0a      ≡⟨ solve! S ⟩
         a · 0a  ≡⟨ cong (λ b → a · b) (sym 1≡0) ⟩
-        a · 1a  ≡⟨ step2 a ⟩
+        a · 1a  ≡⟨ solve! S ⟩
         a       ∎
           where S = CommAlgebra→CommRing A
-                open CommRingStr (snd S) renaming (_·_ to _·s_)
-                step1 : (x : ⟨ A ⟩) → 0r ≡ x ·s 0r
-                step1 = solve S
-                step2 : (x : ⟨ A ⟩) → x ·s 1r ≡ x
-                step2 = solve S
 
       equivFrom1≡0 : CommAlgebraEquiv A UnitCommAlgebra
       equivFrom1≡0 = isContr→Equiv 1≡0→isContr isContrUnit*  ,

Cubical/Algebra/CommAlgebra/Localisation.agda

@@ -31,7 +31,7 @@ open import Cubical.Algebra.Algebra
 open import Cubical.Algebra.CommAlgebra.Base
 open import Cubical.Algebra.CommAlgebra.Properties
 
-open import Cubical.Tactics.CommRingSolver.Reflection
+open import Cubical.Tactics.CommRingSolver
 
 open import Cubical.HITs.SetQuotients as SQ
 open import Cubical.HITs.PropositionalTruncation as PT
@@ -308,10 +308,7 @@ module DoubleAlgLoc (R : CommRing ℓ) (f g : (fst R)) where
      helper2 : (α : FinVec (fst R) 1)
              → x ^ n ≡ linearCombination R α (replicateFinVec 1 y)
              → x ∈ᵢ √ ⟨ y · x ⟩
-     helper2 α p = ∣ (suc n) , ∣ α , cong (x ·_) p ∙ useSolver x y (α zero) ∣₁ ∣₁
-      where
-      useSolver : ∀ x y a → x · (a · y + 0r) ≡ a · (y · x) + 0r
-      useSolver = solve R
+     helper2 α p = ∣ (suc n) , ∣ α , cong (x ·_) p ∙ solve! R ∣₁ ∣₁
 
   toUnit2 : ∀ s → s ∈ [_ⁿ|n≥0] R g → s ⋆ 1a ∈ R[1/fg]ˣ
   toUnit2 s s∈[gⁿ|n≥0] = subst-∈ R[1/fg]ˣ (sym (·IdR (s /1ᶠᵍ)))

Cubical/Algebra/CommAlgebra/LocalisationAlgebra.agda

@@ -28,8 +28,6 @@ open import Cubical.Algebra.CommRing as CommRing hiding (_ˣ;module Units)
 open import Cubical.Algebra.CommRing.Localisation using (isMultClosedSubset)
 open import Cubical.Algebra.Ring
 
-open import Cubical.Tactics.CommRingSolver.Reflection
-
 module Cubical.Algebra.CommAlgebra.LocalisationAlgebra
   {ℓR : Level}
   (R : CommRing ℓR)

Cubical/Algebra/CommAlgebra/QuotientAlgebra.agda

@@ -22,7 +22,7 @@ open import Cubical.Algebra.CommAlgebra.Instances.Unit
 open import Cubical.Algebra.Algebra.Base using (IsAlgebraHom; isPropIsAlgebraHom)
 open import Cubical.Algebra.Ring
 open import Cubical.Algebra.Ring.Ideal using (isIdeal)
-open import Cubical.Tactics.CommRingSolver.Reflection
+open import Cubical.Tactics.CommRingSolver
 open import Cubical.Algebra.Algebra.Properties
 open AlgebraHoms using (_∘a_)
 
@@ -242,8 +242,6 @@ module _
     unfolding quotientHom
 
     isZeroFromIdeal : (x : ⟨ A ⟩) → x ∈ (fst I) → fst (quotientHom A I) x ≡ CommAlgebraStr.0a (snd (A / I))
-    isZeroFromIdeal x x∈I = eq/ x 0a (subst (_∈ fst I) (step x) x∈I )
+    isZeroFromIdeal x x∈I = eq/ x 0a (subst (_∈ fst I) (solve! (CommAlgebra→CommRing A)) x∈I )
       where
         open CommAlgebraStr (snd A)
-        step : (x : ⟨ A ⟩) → x ≡ x - 0a
-        step = solve (CommAlgebra→CommRing A)

Cubical/Algebra/CommAlgebra/UnivariatePolyList.agda

@@ -17,7 +17,7 @@ open import Cubical.Algebra.CommRing.Instances.Polynomials.UnivariatePolyList
 open import Cubical.Algebra.Polynomials.UnivariateList.Base
 open import Cubical.Algebra.Polynomials.UnivariateList.Properties
 
-open import Cubical.Tactics.CommRingSolver.Reflection
+open import Cubical.Tactics.CommRingSolver
 
 private variable
   ℓ ℓ' : Level
@@ -217,7 +217,7 @@ module _ (R : CommRing ℓ) where
             (is-set _ _)
           where
             useSolver : (r : ⟨ R ⟩) → r ≡ (r · 1r) + 0r
-            useSolver = solve R
+            useSolver r = solve! R
 
 
     {- Reforumlation in terms of the R-AlgebraHom from R[X] to A -}