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