Add commutative monoid conversions

3 files changed, 193 insertions, 42 deletions

diff --git a/Data/CMonoid.agda b/Data/CMonoid.agda
new file mode 100644
index 0000000..6aec0c8
--- /dev/null
+++ b/Data/CMonoid.agda
@@ -0,0 +1,78 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level)
+module Data.CMonoid {c ℓ : Level} where
+
+open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory)
+open import Category.Instance.Setoids.SymmetricMonoidal {c} {ℓ} using (Setoids-×; ×-symmetric′)
+open import Object.Monoid.Commutative using (CommutativeMonoid; CommutativeMonoid⇒)
+open import Categories.Object.Monoid using (Monoid)
+
+open import Data.Monoid {c} {ℓ} using (toMonoid; fromMonoid; toMonoid⇒)
+module Setoids-× = SymmetricMonoidalCategory Setoids-×
+
+import Algebra.Bundles as Alg
+
+open import Data.Setoid using (∣_∣)
+open import Relation.Binary using (Setoid)
+open import Function using (Func; _⟨$⟩_)
+open import Data.Product using (curry′; uncurry′; _,_)
+open Func
+
+-- A commutative monoid object in the (symmetric monoidal) category of setoids
+-- is just a commutative monoid
+
+toCMonoid : CommutativeMonoid Setoids-×.symmetric → Alg.CommutativeMonoid c ℓ
+toCMonoid M = record
+    { M
+    ; isCommutativeMonoid = record
+        { isMonoid = M.isMonoid
+        ; comm = comm
+        }
+    }
+  where
+    open CommutativeMonoid M using (monoid; commutative; μ)
+    module M = Alg.Monoid (toMonoid monoid)
+    opaque
+      unfolding toMonoid
+      comm : (x y : M.Carrier) → x M.∙ y M.≈ y M.∙ x
+      comm x y = commutative {x , y}
+
+open import Function.Construct.Constant using () renaming (function to Const)
+open import Categories.Category.Instance.SingletonSet using () renaming (SingletonSetoid to ⊤ₛ)
+
+fromCMonoid : Alg.CommutativeMonoid c ℓ → CommutativeMonoid Setoids-×.symmetric
+fromCMonoid M = record
+    { M
+    ; isCommutativeMonoid = record
+        { isMonoid = M.isMonoid
+        ; commutative = commutative
+        }
+    }
+  where
+    open Alg.CommutativeMonoid M using (monoid; comm)
+    module M = Monoid (fromMonoid monoid)
+    open Setoids-× using (_≈_; _∘_; module braiding)
+    opaque
+      unfolding toMonoid
+      commutative : M.μ ≈ M.μ ∘ braiding.⇒.η _
+      commutative {x , y} = comm x y
+
+-- A morphism of monoids in the (monoidal) category of setoids is a monoid homomorphism
+
+module  _ (M N : CommutativeMonoid Setoids-×.symmetric) where
+
+  module M = Alg.CommutativeMonoid (toCMonoid M)
+  module N = Alg.CommutativeMonoid (toCMonoid N)
+
+  open import Data.Product using (Σ; _,_)
+  open import Function using (_⟶ₛ_)
+  open import Algebra.Morphism using (IsMonoidHomomorphism)
+  open CommutativeMonoid
+  open CommutativeMonoid⇒
+
+  toCMonoid⇒
+      : CommutativeMonoid⇒ Setoids-×.symmetric M N
+      → Σ (M.setoid ⟶ₛ N.setoid) (λ f
+      → IsMonoidHomomorphism M.rawMonoid N.rawMonoid (to f))
+  toCMonoid⇒ f = toMonoid⇒ (monoid M) (monoid N) (monoid⇒ f)
diff --git a/Data/Monoid.agda b/Data/Monoid.agda
index ae2ded9..dba3e79 100644
--- a/Data/Monoid.agda
+++ b/Data/Monoid.agda
@@ -4,7 +4,7 @@ open import Level using (Level)
 module Data.Monoid {c ℓ : Level} where
 
 open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory)
-open import Category.Instance.Setoids.SymmetricMonoidal {c} {ℓ} using (Setoids-×)
+open import Category.Instance.Setoids.SymmetricMonoidal {c} {ℓ} using (Setoids-×; ×-monoidal′)
 open import Categories.Object.Monoid using (Monoid; Monoid⇒)
 
 module Setoids-× = SymmetricMonoidalCategory Setoids-×
@@ -14,31 +14,50 @@ import Algebra.Bundles as Alg
 open import Data.Setoid using (∣_∣)
 open import Relation.Binary using (Setoid)
 open import Function using (Func)
-open import Data.Product using (curry′; _,_)
+open import Data.Product using (curry′; uncurry′; _,_)
 open Func
 
 -- A monoid object in the (monoidal) category of setoids is just a monoid
 
-toMonoid : Monoid Setoids-×.monoidal → Alg.Monoid c ℓ
-toMonoid M = record
-    { Carrier = Carrier
-    ; _≈_ = _≈_
-    ; _∙_ = curry′ (to μ)
-    ; ε = to η _
-    ; isMonoid = record
-        { isSemigroup = record
-            { isMagma = record
-                { isEquivalence = isEquivalence
-                ; ∙-cong = curry′ (cong μ)
-                }
-            ; assoc = λ x y z → assoc {(x , y) , z}
-            }
-        ; identity = (λ x → sym (identityˡ {_ , x}) ) , λ x → sym (identityʳ {x , _})
-        }
-    }
-  where
-    open Monoid M renaming (Carrier to A)
-    open Setoid A
+open import Function.Construct.Constant using () renaming (function to Const)
+open import Categories.Category.Instance.SingletonSet using () renaming (SingletonSetoid to ⊤ₛ)
+
+opaque
+  unfolding ×-monoidal′
+  toMonoid : Monoid Setoids-×.monoidal → Alg.Monoid c ℓ
+  toMonoid M = record
+      { Carrier = Carrier
+      ; _≈_ = _≈_
+      ; _∙_ = curry′ (to μ)
+      ; ε = to η _
+      ; isMonoid = record
+          { isSemigroup = record
+              { isMagma = record
+                  { isEquivalence = isEquivalence
+                  ; ∙-cong = curry′ (cong μ)
+                  }
+              ; assoc = λ x y z → assoc {(x , y) , z}
+              }
+          ; identity = (λ x → sym (identityˡ {_ , x}) ) , λ x → sym (identityʳ {x , _})
+          }
+      }
+    where
+      open Monoid M renaming (Carrier to A)
+      open Setoid A
+
+  fromMonoid : Alg.Monoid c ℓ → Monoid Setoids-×.monoidal
+  fromMonoid M = record
+      { Carrier = setoid
+      ; isMonoid = record
+          { μ = record { to = uncurry′ _∙_ ; cong = uncurry′ ∙-cong }
+          ; η = Const ⊤ₛ setoid ε
+          ; assoc = λ { {(x , y) , z} → assoc x y z }
+          ; identityˡ = λ { {_ , x} → sym (identityˡ x) }
+          ; identityʳ = λ { {x , _} → sym (identityʳ x) }
+          }
+      }
+    where
+      open Alg.Monoid M
 
 -- A morphism of monoids in the (monoidal) category of setoids is a monoid homomorphism
 
@@ -48,19 +67,22 @@ module  _ (M N : Monoid Setoids-×.monoidal) where
   module N = Alg.Monoid (toMonoid N)
 
   open import Data.Product using (Σ; _,_)
-  open import Function using (_⟶ₛ_; _⟨$⟩_)
+  open import Function using (_⟶ₛ_)
   open import Algebra.Morphism using (IsMonoidHomomorphism)
   open Monoid⇒
-  toMonoid⇒
-      : Monoid⇒ Setoids-×.monoidal M N
-      → Σ (M.setoid ⟶ₛ N.setoid) (λ f
-      → IsMonoidHomomorphism M.rawMonoid N.rawMonoid (to f))
-  toMonoid⇒ f = arr f , record
-      { isMagmaHomomorphism = record
-          { isRelHomomorphism = record
-              { cong = cong (arr f)
-              }
-          ; homo = λ x y → preserves-μ f {x , y}
-          }
-      ; ε-homo = preserves-η f
-      }
+
+  opaque
+
+    unfolding toMonoid
+
+    toMonoid⇒
+        : Monoid⇒ Setoids-×.monoidal M N
+        → Σ (M.setoid ⟶ₛ N.setoid) (λ f
+        → IsMonoidHomomorphism M.rawMonoid N.rawMonoid (to f))
+    toMonoid⇒ f = arr f , record
+        { isMagmaHomomorphism = record
+            { isRelHomomorphism = record { cong = cong (arr f) }
+            ; homo = λ x y → preserves-μ f {x , y}
+            }
+        ; ε-homo = preserves-η f
+        }
diff --git a/Data/System/Values.agda b/Data/System/Values.agda
index 737e34e..545a835 100644
--- a/Data/System/Values.agda
+++ b/Data/System/Values.agda
@@ -6,28 +6,30 @@ open import Level using (0ℓ)
 module Data.System.Values (A : CommutativeMonoid 0ℓ 0ℓ) where
 
 import Algebra.Properties.CommutativeMonoid.Sum as Sum
-import Data.Vec.Functional.Properties as VecProps
+import Data.Vec.Functional.Relation.Binary.Equality.Setoid as Pointwise
 import Relation.Binary.PropositionalEquality as ≡
 
-open import Data.Fin using (_↑ˡ_; _↑ʳ_; zero; suc)
+open import Data.Fin using (_↑ˡ_; _↑ʳ_; zero; suc; splitAt)
 open import Data.Nat using (ℕ; _+_; suc)
 open import Data.Product using (_,_)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
 open import Data.Setoid using (∣_∣)
+open import Data.Sum using (inj₁; inj₂)
 open import Data.Vec.Functional as Vec using (Vector; zipWith; replicate)
-open import Data.Vec.Functional.Relation.Binary.Equality.Setoid using (≋-setoid)
 open import Function using (Func; _⟶ₛ_; _⟨$⟩_; _∘_)
 open import Level using (0ℓ)
-open import Relation.Binary using (Rel; Setoid)
+open import Relation.Binary using (Rel; Setoid; IsEquivalence)
 
 open CommutativeMonoid A renaming (Carrier to Value)
 open Func
 open Sum A using (sum)
 
+open Pointwise setoid using (≋-setoid; ≋-isEquivalence)
+
 opaque
 
   Values : ℕ → Setoid 0ℓ 0ℓ
-  Values = ≋-setoid (≡.setoid Value)
+  Values = ≋-setoid
 
 module _ {n : ℕ} where
 
@@ -60,6 +62,53 @@ module _ {n : ℕ} where
 opaque
 
   unfolding Values
+  open Setoid
+  ≋-isEquiv : ∀ n → IsEquivalence (_≈_ (Values n))
+  ≋-isEquiv = ≋-isEquivalence
+
+module _ {n : ℕ} where
+
+  opaque
+    unfolding _⊕_
+
+    ⊕-cong : {x y u v : ≋.Carrier {n}} → x ≋ y → u ≋ v → x ⊕ u ≋ y ⊕ v
+    ⊕-cong x≋y u≋v i = ∙-cong (x≋y i) (u≋v i)
+
+    ⊕-assoc : (x y z : ≋.Carrier {n}) → (x ⊕ y) ⊕ z ≋ x ⊕ (y ⊕ z)
+    ⊕-assoc x y z i = assoc (x i) (y i) (z i)
+
+    ⊕-identityˡ : (x : ≋.Carrier {n}) → <ε> ⊕ x ≋ x
+    ⊕-identityˡ x i = identityˡ (x i)
+
+    ⊕-identityʳ : (x : ≋.Carrier {n}) → x ⊕ <ε> ≋ x
+    ⊕-identityʳ x i = identityʳ (x i)
+
+    ⊕-comm : (x y : ≋.Carrier {n}) → x ⊕ y ≋ y ⊕ x
+    ⊕-comm x y i = comm (x i) (y i)
+
+open CommutativeMonoid
+Valuesₘ : ℕ → CommutativeMonoid 0ℓ 0ℓ
+Valuesₘ n .Carrier = ∣ Values n ∣
+Valuesₘ n ._≈_ = _≋_
+Valuesₘ n ._∙_ = _⊕_
+Valuesₘ n .ε = <ε>
+Valuesₘ n .isCommutativeMonoid = record
+    { isMonoid = record
+        { isSemigroup = record
+            { isMagma = record
+                { isEquivalence = ≋-isEquiv n
+                ; ∙-cong = ⊕-cong
+                }
+            ; assoc = ⊕-assoc
+            }
+        ; identity = ⊕-identityˡ , ⊕-identityʳ
+        }
+    ; comm = ⊕-comm
+    }
+
+opaque
+
+  unfolding Values
 
   [] : ∣ Values 0 ∣
   [] = Vec.[]
@@ -84,7 +133,9 @@ module _ {n m : ℕ} where
         → xs ≋ xs′
         → ys ≋ ys′
         → xs ++ ys ≋ xs′ ++ ys′
-    ++-cong xs xs′ = VecProps.++-cong xs xs′
+    ++-cong xs xs′ xs≋xs′ ys≋ys′ i with splitAt n i
+    ... | inj₁ i = xs≋xs′ i
+    ... | inj₂ i = ys≋ys′ i
 
     splitₛ : Values (n + m) ⟶ₛ Values n ×ₛ Values m
     to splitₛ v = v ∘ (_↑ˡ m) , v ∘ (n ↑ʳ_)