From a643b7e119c5f086c67205072afaed3a1da2252e Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Sat, 6 Dec 2025 16:37:22 -0600
Subject: Add commutative monoid conversions

---
 Data/System/Values.agda | 63 ++++++++++++++++++++++++++++++++++++++++++++-----
 1 file changed, 57 insertions(+), 6 deletions(-)

(limited to 'Data/System/Values.agda')

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
 
@@ -57,6 +59,53 @@ module _ {n : ℕ} where
 
   infix 4 _≋_
 
+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
@@ -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 ↑ʳ_)
-- 
cgit v1.2.3