aboutsummaryrefslogtreecommitdiff
path: root/Functor/Instance/Nat/Pull.agda
diff options
context:
space:
mode:
Diffstat (limited to 'Functor/Instance/Nat/Pull.agda')
-rw-r--r--Functor/Instance/Nat/Pull.agda4
1 files changed, 2 insertions, 2 deletions
diff --git a/Functor/Instance/Nat/Pull.agda b/Functor/Instance/Nat/Pull.agda
index 52f50f1..21007af 100644
--- a/Functor/Instance/Nat/Pull.agda
+++ b/Functor/Instance/Nat/Pull.agda
@@ -10,13 +10,13 @@ open import Categories.Category.Instance.Nat using (Natop)
open import Categories.Functor using (Functor)
open import Category.Construction.CMonoids Setoids-×.symmetric using (CMonoids)
open import Data.CMonoid using (fromCMonoid)
-open import Data.Circuit.Value using (Monoid)
+open import Data.Circuit.Value using (monoid)
open import Data.Fin.Base using (Fin)
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.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; _⟶ₛ_; _⟨$⟩_)