From 6a5154cf29d98ab644b5def52c55f213d1076e2b Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Sun, 9 Nov 2025 17:12:29 -0600
Subject: Clean up System functors

---
 Data/Circuit/Value.agda | 29 ++++++++++++++++++++++++++---
 1 file changed, 26 insertions(+), 3 deletions(-)

(limited to 'Data/Circuit/Value.agda')

diff --git a/Data/Circuit/Value.agda b/Data/Circuit/Value.agda
index 512a622..b135c35 100644
--- a/Data/Circuit/Value.agda
+++ b/Data/Circuit/Value.agda
@@ -2,12 +2,22 @@
 
 module Data.Circuit.Value where
 
-open import Relation.Binary.Lattice.Bundles using (BoundedJoinSemilattice)
+import Relation.Binary.Lattice.Properties.BoundedJoinSemilattice as LatticeProp
+
+open import Algebra.Bundles using (CommutativeMonoid)
+open import Algebra.Structures using (IsCommutativeMonoid; IsMonoid; IsSemigroup; IsMagma)
 open import Data.Product.Base using (_×_; _,_)
 open import Data.String.Base using (String)
 open import Level using (0ℓ)
+open import Relation.Binary.Lattice.Bundles using (BoundedJoinSemilattice)
 open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
 
+open CommutativeMonoid
+open IsCommutativeMonoid
+open IsMagma
+open IsMonoid
+open IsSemigroup
+
 data Value : Set where
   U T F X : Value
 
@@ -129,8 +139,8 @@ join-assoc X X T = ≡.refl
 join-assoc X X F = ≡.refl
 join-assoc X X X = ≡.refl
 
-ValueLattice : BoundedJoinSemilattice 0ℓ 0ℓ 0ℓ
-ValueLattice = record
+Lattice : BoundedJoinSemilattice 0ℓ 0ℓ 0ℓ
+Lattice = record
     { Carrier = Value
     ; _≈_ = _≡_
     ; _≤_ = ≤-Value
@@ -155,3 +165,16 @@ ValueLattice = record
             X → U≤X
         }
     }
+
+module Lattice = BoundedJoinSemilattice Lattice
+
+Monoid : CommutativeMonoid 0ℓ 0ℓ
+Monoid .Carrier = Lattice.Carrier
+Monoid ._≈_ = Lattice._≈_
+Monoid ._∙_ = Lattice._∨_
+Monoid .ε = Lattice.⊥
+Monoid .isCommutativeMonoid .isMonoid .isSemigroup .isMagma .isEquivalence = ≡.isEquivalence
+Monoid .isCommutativeMonoid .isMonoid .isSemigroup .isMagma .∙-cong = ≡.cong₂ join
+Monoid .isCommutativeMonoid .isMonoid .isSemigroup .assoc = join-assoc
+Monoid .isCommutativeMonoid .isMonoid .identity = LatticeProp.identity Lattice
+Monoid .isCommutativeMonoid .comm = join-comm
-- 
cgit v1.2.3