Merge branch 'master' of https://github.com/agda/cubical into categor…

…y-path

.gitignore

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

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/CommSemiring/Base.agda

@@ -38,27 +38,46 @@ record CommSemiringStr (A : Type ℓ) : Type (ℓ-suc ℓ) where
 CommSemiring : ∀ ℓ → Type (ℓ-suc ℓ)
 CommSemiring ℓ = TypeWithStr ℓ CommSemiringStr
 
-makeIsCommSemiring : {R : Type ℓ} {0r 1r : R} {_+_ _·_ : R → R → R}
-                 (is-setR : isSet R)
-                 (+Assoc : (x y z : R) → x + (y + z) ≡ (x + y) + z)
-                 (+IdR : (x : R) → x + 0r ≡ x)
-                 (+Comm : (x y : R) → x + y ≡ y + x)
-                 (·Assoc : (x y z : R) → x · (y · z) ≡ (x · y) · z)
-                 (·IdR : (x : R) → x · 1r ≡ x)
-                 (·DistR+ : (x y z : R) → x · (y + z) ≡ (x · y) + (x · z))
-                 (AnnihilL : (x : R) → 0r · x ≡ 0r)
-                 (·Comm : (x y : R) → x · y ≡ y · x)
-               → IsCommSemiring 0r 1r _+_ _·_
+CommSemiring→Semiring : CommSemiring ℓ → Semiring ℓ
+CommSemiring→Semiring CS .fst = CS .fst
+CommSemiring→Semiring CS .snd = str
+  where
+    open IsCommSemiring
+    open CommSemiringStr
+    open SemiringStr
+
+    CS-str = CS .snd
+
+    str : SemiringStr (CS .fst)
+    0r str = CS-str .0r
+    1r str = CS-str .1r
+    _+_ str = CS-str ._+_
+    _·_ str = CS-str ._·_
+    isSemiring str = (CS-str .isCommSemiring) .isSemiring
+
+makeIsCommSemiring :
+  {R : Type ℓ} {0r 1r : R} {_+_ _·_ : R → R → R}
+  (is-setR : isSet R)
+  (+Assoc : (x y z : R) → x + (y + z) ≡ (x + y) + z)
+  (+IdR : (x : R) → x + 0r ≡ x)
+  (+Comm : (x y : R) → x + y ≡ y + x)
+  (·Assoc : (x y z : R) → x · (y · z) ≡ (x · y) · z)
+  (·IdR : (x : R) → x · 1r ≡ x)
+  (·DistR+ : (x y z : R) → x · (y + z) ≡ (x · y) + (x · z))
+  (AnnihilL : (x : R) → 0r · x ≡ 0r)
+  (·Comm : (x y : R) → x · y ≡ y · x)
+  → IsCommSemiring 0r 1r _+_ _·_
 makeIsCommSemiring {_+_ = _+_} {_·_ = _·_}
   is-setR +Assoc +IdR +Comm ·Assoc ·IdR ·DistR+ AnnihilL ·Comm = x
-  where x : IsCommSemiring _ _ _ _
-        IsCommSemiring.isSemiring x =
-          makeIsSemiring
-            is-setR +Assoc +IdR +Comm ·Assoc
-            ·IdR (λ x → ·Comm _ x ∙ (·IdR x))
-            ·DistR+ (λ x y z → (x + y) · z       ≡⟨ ·Comm (x + y) z ⟩
-                               z · (x + y)       ≡⟨ ·DistR+ z x y ⟩
-                               (z · x) + (z · y) ≡[ i ]⟨ (·Comm z x i + ·Comm z y i) ⟩
-                               (x · z) + (y · z) ∎ )
-            ( λ x → ·Comm x _ ∙ AnnihilL x) AnnihilL
-        IsCommSemiring.·Comm x = ·Comm
+  where
+    x : IsCommSemiring _ _ _ _
+    IsCommSemiring.isSemiring x =
+      makeIsSemiring
+        is-setR +Assoc +IdR +Comm ·Assoc
+        ·IdR (λ x → ·Comm _ x ∙ (·IdR x))
+        ·DistR+ (λ x y z → (x + y) · z       ≡⟨ ·Comm (x + y) z ⟩
+                           z · (x + y)       ≡⟨ ·DistR+ z x y ⟩
+                           (z · x) + (z · y) ≡[ i ]⟨ (·Comm z x i + ·Comm z y i) ⟩
+                           (x · z) + (y · z) ∎ )
+        ( λ x → ·Comm x _ ∙ AnnihilL x) AnnihilL
+    IsCommSemiring.·Comm x = ·Comm

Cubical/Algebra/CommSemiring/Instances/Nat.agda

@@ -0,0 +1,30 @@
+{-# OPTIONS --safe #-}
+module Cubical.Algebra.CommSemiring.Instances.Nat where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+
+import Cubical.Data.Nat as Nat
+open import Cubical.Data.Nat using (ℕ; suc; zero)
+
+open import Cubical.Algebra.CommSemiring
+
+ℕasCSR : CommSemiring ℓ-zero
+ℕasCSR .fst  = ℕ
+ℕasCSR .snd  = str
+  where
+    open CommSemiringStr
+
+    str : CommSemiringStr ℕ
+    0r str = zero
+    1r str = suc zero
+    _+_ str = Nat._+_
+    _·_ str = Nat._·_
+    isCommSemiring str =
+      makeIsCommSemiring
+        Nat.isSetℕ
+        Nat.+-assoc Nat.+-zero Nat.+-comm
+        Nat.·-assoc Nat.·-identityʳ
+        (λ x y z → sym (Nat.·-distribˡ x y z))
+        (λ _ → refl)
+        Nat.·-comm