aboutsummaryrefslogtreecommitdiff
path: root/Data/System/Monoidal.agda
diff options
context:
space:
mode:
Diffstat (limited to 'Data/System/Monoidal.agda')
-rw-r--r--Data/System/Monoidal.agda2
1 files changed, 1 insertions, 1 deletions
diff --git a/Data/System/Monoidal.agda b/Data/System/Monoidal.agda
index f4f5311..31b6c20 100644
--- a/Data/System/Monoidal.agda
+++ b/Data/System/Monoidal.agda
@@ -19,7 +19,7 @@ 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.System.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)