From a07a9d6ea38c55aeac59cb93678b9c830ce54705 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Tue, 7 Jul 2026 13:32:20 -0700 Subject: Update circuit values --- Functor/Instance/Nat/System.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'Functor/Instance/Nat/System.agda') 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 (_∙_) -- cgit v1.2.3