diff options
Diffstat (limited to 'Functor/Instance/Nat')
| -rw-r--r-- | Functor/Instance/Nat/Pull.agda | 2 | ||||
| -rw-r--r-- | Functor/Instance/Nat/Push.agda | 2 | ||||
| -rw-r--r-- | Functor/Instance/Nat/System.agda | 2 |
3 files changed, 3 insertions, 3 deletions
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 (_∙_) |