Update circuit values

3 files changed, 6 insertions, 6 deletions

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)