aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Category/Instance/Monoids.agda6
-rw-r--r--Data/Circuit/Value.agda178
-rw-r--r--Data/System/Core.agda4
-rw-r--r--Data/System/Looped.agda4
-rw-r--r--Data/System/Monoidal.agda4
-rw-r--r--Functor/Instance/Nat/Pull.agda4
-rw-r--r--Functor/Instance/Nat/Push.agda4
-rw-r--r--Functor/Instance/Nat/System.agda4
-rw-r--r--Lattice/Bundle/BoundedDistributive.agda50
-rw-r--r--Lattice/Structure/IsBoundedDistributive.agda4
-rw-r--r--NaturalTransformation/Instance/GateSemantics.agda2
11 files changed, 201 insertions, 63 deletions
diff --git a/Category/Instance/Monoids.agda b/Category/Instance/Monoids.agda
index 28f214b..f084b79 100644
--- a/Category/Instance/Monoids.agda
+++ b/Category/Instance/Monoids.agda
@@ -12,8 +12,10 @@ open import Algebra using (Monoid)
open import Categories.Category using (Category)
open import Categories.Category.Helper using (categoryHelper)
open import Relation.Binary using (IsEquivalence)
+open import Function using (Func; _⟶ₛ_)
open Monoid hiding (_≈_)
+open Func
record MonoidHomomorphism (M N : Monoid c ℓ) : Set (c ⊔ ℓ) where
@@ -24,6 +26,10 @@ record MonoidHomomorphism (M N : Monoid c ℓ) : Set (c ⊔ ℓ) where
open Raw.MonoidHomomorphism rawMonoidHomomorphism public
+ func : setoid M ⟶ₛ setoid N
+ func .to = ⟦_⟧
+ func .cong = ⟦⟧-cong
+
module _ {M N : Monoid c ℓ} where
-- Pointwise equality of monoid homomorphisms
diff --git a/Data/Circuit/Value.agda b/Data/Circuit/Value.agda
index b135c35..1bf1a6a 100644
--- a/Data/Circuit/Value.agda
+++ b/Data/Circuit/Value.agda
@@ -4,20 +4,15 @@ module Data.Circuit.Value where
import Relation.Binary.Lattice.Properties.BoundedJoinSemilattice as LatticeProp
-open import Algebra.Bundles using (CommutativeMonoid)
+open import Algebra.Bundles using (CommutativeMonoid; Semiring)
+open import Algebra.Lattice.Bundles using (Semilattice)
open import Algebra.Structures using (IsCommutativeMonoid; IsMonoid; IsSemigroup; IsMagma)
open import Data.Product.Base using (_×_; _,_)
open import Data.String.Base using (String)
+open import Lattice.Bundle.BoundedDistributive using (BoundedDistributiveLattice)
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
@@ -49,35 +44,86 @@ showValue X = "X"
join : Value → Value → Value
join U y = y
-join x U = x
+join T U = T
join T T = T
join T F = X
+join T X = X
+join F U = F
join F T = X
join F F = F
+join F X = X
join X _ = X
-join _ X = X
+
+meet : Value → Value → Value
+meet U _ = U
+meet T U = U
+meet T T = T
+meet T F = U
+meet T X = T
+meet F U = U
+meet F T = U
+meet F F = F
+meet F X = F
+meet X y = y
+
+implies : Value → Value → Value
+implies U _ = X
+implies T U = U
+implies T T = X
+implies T F = F
+implies T X = X
+implies F U = U
+implies F T = T
+implies F F = X
+implies F X = X
+implies X U = U
+implies X T = T
+implies X F = F
+implies X X = X
+
+≤-infimum
+ : (x y : Value)
+ → ≤-Value (meet x y) x
+ × ≤-Value (meet x y) y
+ × ((z : Value) → ≤-Value z x → ≤-Value z y → ≤-Value z (meet x y))
+≤-infimum U U = v≤v , v≤v , λ _ z≤x _ → z≤x
+≤-infimum U T = v≤v , U≤T , λ _ z≤x _ → z≤x
+≤-infimum U F = v≤v , U≤F , λ _ z≤x _ → z≤x
+≤-infimum U X = v≤v , U≤X , λ _ z≤x _ → z≤x
+≤-infimum T U = U≤T , v≤v , λ _ _ z≤y → z≤y
+≤-infimum T T = v≤v , v≤v , λ _ z≤x _ → z≤x
+≤-infimum T F = U≤T , U≤F , λ { U _ _ → v≤v }
+≤-infimum T X = v≤v , T≤X , λ _ z≤x _ → z≤x
+≤-infimum F U = U≤F , v≤v , λ _ _ z≤y → z≤y
+≤-infimum F T = U≤F , U≤T , λ { U _ _ → v≤v }
+≤-infimum F F = v≤v , v≤v , λ _ z≤x _ → z≤x
+≤-infimum F X = v≤v , F≤X , λ _ z≤x _ → z≤x
+≤-infimum X U = U≤X , v≤v , λ _ _ z≤y → z≤y
+≤-infimum X T = T≤X , v≤v , λ _ _ z≤y → z≤y
+≤-infimum X F = F≤X , v≤v , λ _ _ z≤y → z≤y
+≤-infimum X X = v≤v , v≤v , λ _ z≤x _ → z≤x
≤-supremum
: (x y : Value)
→ ≤-Value x (join x y)
× ≤-Value y (join x y)
× ((z : Value) → ≤-Value x z → ≤-Value y z → ≤-Value (join x y) z)
-≤-supremum U U = v≤v , v≤v , λ _ U≤z _ → U≤z
-≤-supremum U T = U≤T , v≤v , λ { z x≤z y≤z → y≤z }
-≤-supremum U F = U≤F , v≤v , λ { z x≤z y≤z → y≤z }
-≤-supremum U X = U≤X , v≤v , λ { z x≤z y≤z → y≤z }
-≤-supremum T U = v≤v , U≤T , λ { z x≤z y≤z → x≤z }
-≤-supremum T T = v≤v , v≤v , λ { z x≤z y≤z → x≤z }
-≤-supremum T F = T≤X , F≤X , λ { X x≤z y≤z → v≤v }
-≤-supremum T X = T≤X , v≤v , λ { z x≤z y≤z → y≤z }
-≤-supremum F U = v≤v , U≤F , λ { z x≤z y≤z → x≤z }
-≤-supremum F T = F≤X , T≤X , λ { X x≤z y≤z → v≤v }
-≤-supremum F F = v≤v , v≤v , λ { z x≤z y≤z → x≤z }
-≤-supremum F X = F≤X , v≤v , λ { z x≤z y≤z → y≤z }
-≤-supremum X U = v≤v , U≤X , λ { z x≤z y≤z → x≤z }
-≤-supremum X T = v≤v , T≤X , λ { z x≤z y≤z → x≤z }
-≤-supremum X F = v≤v , F≤X , λ { z x≤z y≤z → x≤z }
-≤-supremum X X = v≤v , v≤v , λ { z x≤z y≤z → x≤z }
+≤-supremum U U = v≤v , v≤v , λ _ x≤z _ → x≤z
+≤-supremum U T = U≤T , v≤v , λ _ _ y≤z → y≤z
+≤-supremum U F = U≤F , v≤v , λ _ _ y≤z → y≤z
+≤-supremum U X = U≤X , v≤v , λ _ _ y≤z → y≤z
+≤-supremum T U = v≤v , U≤T , λ _ x≤z _ → x≤z
+≤-supremum T T = v≤v , v≤v , λ _ x≤z _ → x≤z
+≤-supremum T F = T≤X , F≤X , λ { X _ _ → v≤v }
+≤-supremum T X = T≤X , v≤v , λ _ _ y≤z → y≤z
+≤-supremum F U = v≤v , U≤F , λ _ x≤z _ → x≤z
+≤-supremum F T = F≤X , T≤X , λ { X _ _ → v≤v }
+≤-supremum F F = v≤v , v≤v , λ _ x≤z _ → x≤z
+≤-supremum F X = F≤X , v≤v , λ _ _ y≤z → y≤z
+≤-supremum X U = v≤v , U≤X , λ _ x≤z _ → x≤z
+≤-supremum X T = v≤v , T≤X , λ _ x≤z _ → x≤z
+≤-supremum X F = v≤v , F≤X , λ _ x≤z _ → x≤z
+≤-supremum X X = v≤v , v≤v , λ _ x≤z _ → x≤z
join-comm : (x y : Value) → join x y ≡ join y x
join-comm U U = ≡.refl
@@ -139,15 +185,59 @@ join-assoc X X T = ≡.refl
join-assoc X X F = ≡.refl
join-assoc X X X = ≡.refl
-Lattice : BoundedJoinSemilattice 0ℓ 0ℓ 0ℓ
-Lattice = record
+meet-distribˡ-join : (x y z : Value) → meet x (join y z) ≡ join (meet x y) (meet x z)
+meet-distribˡ-join U _ _ = ≡.refl
+meet-distribˡ-join T U _ = ≡.refl
+meet-distribˡ-join T T U = ≡.refl
+meet-distribˡ-join T T T = ≡.refl
+meet-distribˡ-join T T F = ≡.refl
+meet-distribˡ-join T T X = ≡.refl
+meet-distribˡ-join T F U = ≡.refl
+meet-distribˡ-join T F T = ≡.refl
+meet-distribˡ-join T F F = ≡.refl
+meet-distribˡ-join T F X = ≡.refl
+meet-distribˡ-join T X U = ≡.refl
+meet-distribˡ-join T X T = ≡.refl
+meet-distribˡ-join T X F = ≡.refl
+meet-distribˡ-join T X X = ≡.refl
+meet-distribˡ-join F U _ = ≡.refl
+meet-distribˡ-join F T U = ≡.refl
+meet-distribˡ-join F T T = ≡.refl
+meet-distribˡ-join F T F = ≡.refl
+meet-distribˡ-join F T X = ≡.refl
+meet-distribˡ-join F F U = ≡.refl
+meet-distribˡ-join F F T = ≡.refl
+meet-distribˡ-join F F F = ≡.refl
+meet-distribˡ-join F F X = ≡.refl
+meet-distribˡ-join F X U = ≡.refl
+meet-distribˡ-join F X T = ≡.refl
+meet-distribˡ-join F X F = ≡.refl
+meet-distribˡ-join F X X = ≡.refl
+meet-distribˡ-join X _ _ = ≡.refl
+
+v≤X : (v : Value) → ≤-Value v X
+v≤X U = U≤X
+v≤X T = T≤X
+v≤X F = F≤X
+v≤X X = v≤v
+
+U≤v : (v : Value) → ≤-Value U v
+U≤v U = v≤v
+U≤v T = U≤T
+U≤v F = U≤F
+U≤v X = U≤X
+
+𝕍 : BoundedDistributiveLattice 0ℓ 0ℓ 0ℓ
+𝕍 = record
{ Carrier = Value
; _≈_ = _≡_
; _≤_ = ≤-Value
; _∨_ = join
+ ; _∧_ = meet
+ ; ⊤ = X
; ⊥ = U
- ; isBoundedJoinSemilattice = record
- { isJoinSemilattice = record
+ ; isBoundedDistributiveLattice = record
+ { isLattice = record
{ isPartialOrder = record 
{ isPreorder = record
{ isEquivalence = ≡.isEquivalence
@@ -157,24 +247,18 @@ Lattice = record
; antisym = ≤-antisymmetric
}
; supremum = ≤-supremum
+ ; infimum = ≤-infimum
}
- ; minimum = λ where
- U → v≤v
- T → U≤T
- F → U≤F
- X → U≤X
+ ; maximum = v≤X
+ ; minimum = U≤v
+ ; ∧-distribˡ-∨ = meet-distribˡ-join
}
}
-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
+module 𝕍 = BoundedDistributiveLattice 𝕍
+
+semiring : Semiring 0ℓ 0ℓ
+semiring = 𝕍.semiring
+
+monoid : CommutativeMonoid 0ℓ 0ℓ
+monoid = let open Semiring semiring in +-commutativeMonoid
diff --git a/Data/System/Core.agda b/Data/System/Core.agda
index 6da264c..3616847 100644
--- a/Data/System/Core.agda
+++ b/Data/System/Core.agda
@@ -6,11 +6,11 @@ module Data.System.Core {ℓ : Level} where
import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
-open import Data.Circuit.Value using (Monoid)
+open import Data.Circuit.Value using (monoid)
open import Data.Nat using (ℕ)
open import Data.Setoid using (_⇒ₛ_; ∣_∣)
open import Data.Setoid.Unit using (⊤ₛ)
-open import Data.Values Monoid using (Values; _≋_; module ≋; <ε>)
+open import Data.Values monoid using (Values; _≋_; module ≋; <ε>)
open import Function using (Func; _⟨$⟩_)
open import Function.Construct.Constant using () renaming (function to Const)
open import Function.Construct.Identity using () renaming (function to Id)
diff --git a/Data/System/Looped.agda b/Data/System/Looped.agda
index f69d75b..96f3432 100644
--- a/Data/System/Looped.agda
+++ b/Data/System/Looped.agda
@@ -13,8 +13,8 @@ open import Data.Nat using (ℕ)
open import Data.System.Category {ℓ} using (Systems[_,_])
open import Data.System.Core {ℓ} using (System; _≤_)
open import Categories.Functor using (Functor)
-open import Data.Circuit.Value using (Monoid)
-open import Data.Values Monoid using (_⊕_; ⊕-cong; module ≋)
+open import Data.Circuit.Value using (monoid)
+open import Data.Values monoid using (_⊕_; ⊕-cong; module ≋)
open import Relation.Binary using (Setoid)
open import Function using (Func; _⟨$⟩_) renaming (id to idf)
diff --git a/Data/System/Monoidal.agda b/Data/System/Monoidal.agda
index 731bbe5..cdf06e2 100644
--- a/Data/System/Monoidal.agda
+++ b/Data/System/Monoidal.agda
@@ -15,12 +15,12 @@ open import Categories.Functor using (Functor)
open import Categories.Functor.Bifunctor using (Bifunctor; flip-bifunctor)
open import Categories.Morphism (Systems[ n , m ]) using (_≅_; Iso)
open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; niHelper)
-open import Data.Circuit.Value using (Monoid)
+open import Data.Circuit.Value using (monoid)
open import Data.Product using (_,_; _×_; uncurry′)
open import Data.Product.Function.NonDependent.Setoid using (_×-function_; proj₁ₛ; proj₂ₛ; swapₛ)
open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
open import Data.Setoid using (_⇒ₛ_; _×-⇒_; assocₛ⇒; assocₛ⇐)
-open import Data.Values Monoid using (Values; _⊕_; ⊕-cong; ⊕-identityˡ; ⊕-identityʳ; ⊕-assoc; ⊕-comm; module ≋)
+open import Data.Values monoid using (Values; _⊕_; ⊕-cong; ⊕-identityˡ; ⊕-identityʳ; ⊕-assoc; ⊕-comm; module ≋)
open import Function using (Func; _⟶ₛ_)
open import Function.Construct.Setoid using (_∙_)
open import Relation.Binary using (Setoid)
diff --git a/Functor/Instance/Nat/Pull.agda b/Functor/Instance/Nat/Pull.agda
index 52f50f1..21007af 100644
--- a/Functor/Instance/Nat/Pull.agda
+++ b/Functor/Instance/Nat/Pull.agda
@@ -10,13 +10,13 @@ open import Categories.Category.Instance.Nat using (Natop)
open import Categories.Functor using (Functor)
open import Category.Construction.CMonoids Setoids-×.symmetric using (CMonoids)
open import Data.CMonoid using (fromCMonoid)
-open import Data.Circuit.Value using (Monoid)
+open import Data.Circuit.Value using (monoid)
open import Data.Fin.Base using (Fin)
open import Data.Monoid using (fromMonoid)
open import Data.Nat.Base using (ℕ)
open import Data.Product using (_,_)
open import Data.Setoid using (∣_∣; _⇒ₛ_)
-open import Data.Values Monoid using (Values; _⊕_; module Object)
+open import Data.Values monoid using (Values; _⊕_; module Object)
open import Data.Unit using (⊤; tt)
open import Function.Base using (id; _∘_)
open import Function.Bundles using (Func; _⟶ₛ_; _⟨$⟩_)
diff --git a/Functor/Instance/Nat/Push.agda b/Functor/Instance/Nat/Push.agda
index c5becb4..be92261 100644
--- a/Functor/Instance/Nat/Push.agda
+++ b/Functor/Instance/Nat/Push.agda
@@ -9,13 +9,13 @@ open import Categories.Category.Instance.Nat using (Nat)
open import Categories.Category.Instance.Setoids using (Setoids)
open import Categories.Functor using (Functor)
open import Category.Construction.CMonoids Setoids-×.symmetric using (CMonoids)
-open import Data.Circuit.Value using (Monoid)
+open import Data.Circuit.Value using (monoid)
open import Data.Fin using (Fin)
open import Data.Fin.Preimage using (preimage; preimage-cong₁)
open import Data.Nat using (ℕ)
open import Data.Setoid using (∣_∣; _⇒ₛ_)
open import Data.Subset.Functional using (⁅_⁆)
-open import Data.Values Monoid using (Values; module Object; _⊕_; <ε>; _≋_; ≋-isEquiv; merge; push; merge-⊕; merge-<ε>; merge-cong; merge-⁅⁆; merge-push; merge-cong₂; lookup)
+open import Data.Values monoid using (Values; module Object; _⊕_; <ε>; _≋_; ≋-isEquiv; merge; push; merge-⊕; merge-<ε>; merge-cong; merge-⁅⁆; merge-push; merge-cong₂; lookup)
open import Function using (Func; _⟶ₛ_; _⟨$⟩_; _∘_; id)
open import Function.Construct.Identity using () renaming (function to Id)
open import Function.Construct.Setoid using (_∙_)
diff --git a/Functor/Instance/Nat/System.agda b/Functor/Instance/Nat/System.agda
index 35768f8..34ae65a 100644
--- a/Functor/Instance/Nat/System.agda
+++ b/Functor/Instance/Nat/System.agda
@@ -28,7 +28,7 @@ open import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal using (
open import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal.Symmetric using () renaming (module Strong to Strong₄)
open import Category.Construction.CMonoids (Setoids-×.symmetric {suc 0ℓ} {suc 0ℓ}) using (CMonoids)
open import Category.Instance.SymMonCat using () renaming (module Strong to Strong₁)
-open import Data.Circuit.Value using (Monoid)
+open import Data.Circuit.Value using (monoid)
open import Data.Fin using (Fin)
open import Data.Nat using (ℕ)
open import Data.Product using (_,_; _×_)
@@ -36,7 +36,7 @@ open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
open import Data.Setoid using (∣_∣)
open import Data.Setoid.Unit using (⊤ₛ)
open import Data.System {suc 0ℓ} using (System; _≤_; _≈_; Systems[_,_]; ≤-refl; ≤-trans; discrete; Systems-MC; Systems-SMC)
-open import Data.Values Monoid using (module ≋; module Object; Values; ≋-isEquiv)
+open import Data.Values monoid using (module ≋; module Object; Values; ≋-isEquiv)
open import Function using (Func; _⟶ₛ_; _⟨$⟩_; _∘_; id)
open import Function.Construct.Identity using () renaming (function to Id)
open import Function.Construct.Setoid using (_∙_)
diff --git a/Lattice/Bundle/BoundedDistributive.agda b/Lattice/Bundle/BoundedDistributive.agda
index e2ac964..bb9f4a2 100644
--- a/Lattice/Bundle/BoundedDistributive.agda
+++ b/Lattice/Bundle/BoundedDistributive.agda
@@ -2,7 +2,16 @@
module Lattice.Bundle.BoundedDistributive where
+import Relation.Binary.Lattice.Properties.BoundedJoinSemilattice as BJS
+import Relation.Binary.Lattice.Properties.BoundedLattice as BL
+import Relation.Binary.Lattice.Properties.BoundedMeetSemilattice as BMS
+import Relation.Binary.Lattice.Properties.DistributiveLattice as DL
+import Relation.Binary.Lattice.Properties.JoinSemilattice as JS
+import Relation.Binary.Lattice.Properties.MeetSemilattice as MS
+
open import Algebra using (Op₂)
+open import Algebra.Bundles using (Semiring)
+open import Data.Product using (_,_)
open import Lattice.Structure.IsBoundedDistributive using (IsBoundedDistributiveLattice)
open import Level using (suc; _⊔_)
open import Relation.Binary using (Rel)
@@ -35,4 +44,43 @@ record BoundedDistributiveLattice c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔
}
open BoundedLattice boundedLattice public
- using (lattice; joinSemilattice; meetSemilattice; poset; preorder; setoid)
+ using (lattice; boundedJoinSemilattice; boundedMeetSemilattice; joinSemilattice; meetSemilattice; poset; preorder; setoid)
+
+ semiring : Semiring c ℓ₁
+ semiring = record
+ { Carrier = Carrier
+ ; _≈_ = _≈_
+ ; _+_ = _∨_
+ ; _*_ = _∧_
+ ; 0# = ⊥
+ ; 1# = ⊤
+ ; isSemiring = record
+ { isSemiringWithoutAnnihilatingZero = record
+ { +-isCommutativeMonoid = record
+ { isMonoid = record
+ { isSemigroup = record
+ { isMagma = record
+ { isEquivalence = isEquivalence
+ ; ∙-cong = ∨-cong
+ }
+ ; assoc = ∨-assoc
+ }
+ ; identity = ∨-identity
+ }
+ ; comm = ∨-comm
+ }
+ ; *-cong = ∧-cong
+ ; *-assoc = ∧-assoc
+ ; *-identity = ∧-identity
+ ; distrib = ∧-distribˡ-∨ , ∧-distribʳ-∨
+ }
+ ; zero = ∧-zero
+ }
+ }
+ where
+ open BJS boundedJoinSemilattice using () renaming (identity to ∨-identity)
+ open BL boundedLattice using (∧-zero)
+ open BMS boundedMeetSemilattice using () renaming (identity to ∧-identity)
+ open DL distributiveLattice using (∧-distribʳ-∨)
+ open JS joinSemilattice using (∨-comm; ∨-cong; ∨-assoc)
+ open MS meetSemilattice using (∧-comm; ∧-cong; ∧-assoc)
diff --git a/Lattice/Structure/IsBoundedDistributive.agda b/Lattice/Structure/IsBoundedDistributive.agda
index dfd67d8..6128187 100644
--- a/Lattice/Structure/IsBoundedDistributive.agda
+++ b/Lattice/Structure/IsBoundedDistributive.agda
@@ -27,8 +27,6 @@ record IsBoundedDistributiveLattice
minimum : Minimum _≤_ ⊥
∧-distribˡ-∨ : _DistributesOverˡ_ _≈_ _∧_ _∨_
- open IsLattice isLattice public
-
isBoundedLattice : IsBoundedLattice _∨_ _∧_ ⊤ ⊥
isBoundedLattice = record
{ isLattice = isLattice
@@ -41,3 +39,5 @@ record IsBoundedDistributiveLattice
{ isLattice = isLattice
; ∧-distribˡ-∨ = ∧-distribˡ-∨
}
+
+ open IsBoundedLattice isBoundedLattice public
diff --git a/NaturalTransformation/Instance/GateSemantics.agda b/NaturalTransformation/Instance/GateSemantics.agda
index 9cdbc1b..70c70bf 100644
--- a/NaturalTransformation/Instance/GateSemantics.agda
+++ b/NaturalTransformation/Instance/GateSemantics.agda
@@ -23,7 +23,7 @@ open import Data.Nat using (ℕ)
open import Data.Setoid using (∣_∣; _⇒ₛ_)
open import Data.Setoid.Unit using (⊤ₛ)
open import Data.System {suc 0ℓ} using (System)
-open import Data.Values Value.Monoid using (Values)
+open import Data.Values Value.monoid using (Values)
open import Function using (Func; _⟶ₛ_; id; _⟨$⟩_)
open import Function.Construct.Constant using () renaming (function to Const)
open import Function.Construct.Identity using () renaming (function to Id)
generated by cgit v1.2.3 (git 2.39.1) at 2026-07-21 21:54:27 +0000