Move values module

7 files changed, 7 insertions, 7 deletions

diff --git a/Data/System.agda b/Data/System.agda
index d12fa12..a2adec3 100644
--- a/Data/System.agda
+++ b/Data/System.agda
@@ -12,7 +12,7 @@ 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.System.Values Monoid using (Values; _≋_; module ≋; <ε>)
+open import Data.Values Monoid using (Values; _≋_; module ≋; <ε>)
 open import Function using (Func; _⟨$⟩_; flip)
 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/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)
diff --git a/Data/System/Values.agda b/Data/Values.agda
index d1cd6c9..6003181 100644
--- a/Data/System/Values.agda
+++ b/Data/Values.agda
@@ -3,7 +3,7 @@
 open import Algebra.Bundles using (CommutativeMonoid)
 open import Level using (0ℓ)
 
-module Data.System.Values (A : CommutativeMonoid 0ℓ 0ℓ) where
+module Data.Values (A : CommutativeMonoid 0ℓ 0ℓ) where
 
 open import Category.Instance.Setoids.SymmetricMonoidal {0ℓ} {0ℓ} using (Setoids-×)
 
diff --git a/Functor/Instance/Nat/Pull.agda b/Functor/Instance/Nat/Pull.agda
index c2a06c6..52f50f1 100644
--- a/Functor/Instance/Nat/Pull.agda
+++ b/Functor/Instance/Nat/Pull.agda
@@ -16,7 +16,7 @@ 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.System.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 c417ebf..c5becb4 100644
--- a/Functor/Instance/Nat/Push.agda
+++ b/Functor/Instance/Nat/Push.agda
@@ -15,7 +15,7 @@ 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.System.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 728fec8..a3c65ca 100644
--- a/Functor/Instance/Nat/System.agda
+++ b/Functor/Instance/Nat/System.agda
@@ -37,7 +37,7 @@ open import Data.Setoid using (∣_∣)
 open import Data.Setoid.Unit using (⊤ₛ)
 open import Data.System {suc 0ℓ} using (System; _≤_; Systemₛ; Systems; ≤-refl; ≤-trans; _≈_; discrete)
 open import Data.System.Monoidal {suc 0ℓ} using (Systems-MC; Systems-SMC)
-open import Data.System.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/NaturalTransformation/Instance/GateSemantics.agda b/NaturalTransformation/Instance/GateSemantics.agda
index e86e942..c85526c 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.System.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)