4 files changed, 15 insertions, 19 deletions
diff --git a/Functor/Instance/Nat/Preimage.agda b/Functor/Instance/Nat/Preimage.agda
index 7d471b9..7da00f4 100644
--- a/Functor/Instance/Nat/Preimage.agda
+++ b/Functor/Instance/Nat/Preimage.agda
@@ -2,8 +2,7 @@
 
 module Functor.Instance.Nat.Preimage where
 
-open import Categories.Category.Core using (module Category)
-open import Categories.Category.Instance.Nat using (Nat)
+open import Categories.Category.Instance.Nat using (Natop)
 open import Categories.Category.Instance.Setoids using (Setoids)
 open import Categories.Functor using (Functor)
 open import Data.Fin.Base using (Fin)
@@ -11,7 +10,7 @@ open import Data.Bool.Base using (Bool)
 open import Data.Nat.Base using (ℕ)
 open import Data.Subset.Functional using (Subset)
 open import Data.Vec.Functional.Relation.Binary.Equality.Setoid using (≋-setoid)
-open import Function.Base using (id; flip; _∘_)
+open import Function.Base using (id; _∘_)
 open import Function.Bundles using (Func; _⟶ₛ_)
 open import Function.Construct.Identity using () renaming (function to Id)
 open import Function.Construct.Setoid using (setoid; _∙_)
@@ -22,8 +21,6 @@ open import Relation.Binary.PropositionalEquality as ≡ using (_≗_)
 open Functor
 open Func
 
-module Nat = Category Nat
-
 _≈_ : {X Y : Setoid 0ℓ 0ℓ} → Rel (X ⟶ₛ Y) 0ℓ
 _≈_ {X} {Y} = Setoid._≈_ (setoid X Y)
 infixr 4 _≈_
@@ -60,7 +57,7 @@ Preimage-resp-≈
 Preimage-resp-≈ f≗g {v} = ≡.cong v ∘ f≗g
 
 -- the Preimage functor
-Preimage : Functor Nat.op (Setoids 0ℓ 0ℓ)
+Preimage : Functor Natop (Setoids 0ℓ 0ℓ)
 F₀ Preimage = Subsetₛ
 F₁ Preimage = Preimage₁
 identity Preimage = Preimage-identity
diff --git a/Functor/Instance/Nat/Pull.agda b/Functor/Instance/Nat/Pull.agda
index cf15809..5b74399 100644
--- a/Functor/Instance/Nat/Pull.agda
+++ b/Functor/Instance/Nat/Pull.agda
@@ -2,29 +2,24 @@
 
 module Functor.Instance.Nat.Pull where
 
-open import Categories.Category.Core using (module Category)
-open import Categories.Category.Instance.Nat using (Nat)
+open import Categories.Category.Instance.Nat using (Natop)
 open import Categories.Category.Instance.Setoids using (Setoids)
 open import Categories.Functor using (Functor)
-open import Data.Circuit.Merge using (merge; merge-cong₁; merge-cong₂; merge-⁅⁆; merge-preimage)
 open import Data.Fin.Base using (Fin)
-open import Data.Fin.Preimage using (preimage; preimage-cong₁)
 open import Data.Nat.Base using (ℕ)
-open import Data.Subset.Functional using (⁅_⁆)
-open import Function.Base using (id; flip; _∘_)
+open import Function.Base using (id; _∘_)
 open import Function.Bundles using (Func; _⟶ₛ_)
 open import Function.Construct.Identity using () renaming (function to Id)
 open import Function.Construct.Setoid using (setoid; _∙_)
 open import Level using (0ℓ)
 open import Relation.Binary using (Rel; Setoid)
 open import Relation.Binary.PropositionalEquality as ≡ using (_≗_)
-open import Data.System using (Values)
+open import Data.Circuit.Value using (Value)
+open import Data.System.Values Value using (Values)
 
 open Functor
 open Func
 
-module Nat = Category Nat
-
 _≈_ : {X Y : Setoid 0ℓ 0ℓ} → Rel (X ⟶ₛ Y) 0ℓ
 _≈_ {X} {Y} = Setoid._≈_ (setoid X Y)
 infixr 4 _≈_
@@ -32,6 +27,7 @@ infixr 4 _≈_
 private
   variable A B C : ℕ
 
+
 -- action on objects is Values n (Vector Value n)
 
 -- action of Pull on morphisms (contravariant)
@@ -59,7 +55,7 @@ Pull-resp-≈
 Pull-resp-≈ f≗g {v} = ≡.cong v ∘ f≗g
 
 -- the Pull functor
-Pull : Functor Nat.op (Setoids 0ℓ 0ℓ)
+Pull : Functor Natop (Setoids 0ℓ 0ℓ)
 F₀ Pull = Values
 F₁ Pull = Pull₁
 identity Pull = Pull-identity
diff --git a/Functor/Instance/Nat/Push.agda b/Functor/Instance/Nat/Push.agda
index 8b40bd7..53d0bef 100644
--- a/Functor/Instance/Nat/Push.agda
+++ b/Functor/Instance/Nat/Push.agda
@@ -17,7 +17,8 @@ open import Function.Construct.Setoid using (setoid; _∙_)
 open import Level using (0ℓ)
 open import Relation.Binary using (Rel; Setoid)
 open import Relation.Binary.PropositionalEquality as ≡ using (_≗_)
-open import Data.System using (Values)
+open import Data.Circuit.Value using (Value)
+open import Data.System.Values Value using (Values)
 
 open Func
 open Functor
diff --git a/Functor/Instance/Nat/System.agda b/Functor/Instance/Nat/System.agda
index 2b96355..730f90d 100644
--- a/Functor/Instance/Nat/System.agda
+++ b/Functor/Instance/Nat/System.agda
@@ -5,10 +5,12 @@ module Functor.Instance.Nat.System {ℓ} where
 open import Categories.Category.Instance.Nat using (Nat)
 open import Categories.Category.Instance.Setoids using (Setoids)
 open import Categories.Functor.Core using (Functor)
+open import Data.Circuit.Value using (Value)
 open import Data.Fin.Base using (Fin)
 open import Data.Nat.Base using (ℕ)
 open import Data.Product.Base using (_,_; _×_)
-open import Data.System using (System; ≤-System; Systemₛ; module ≋)
+open import Data.System using (System; ≤-System; Systemₛ)
+open import Data.System.Values Value using (module ≋)
 open import Function.Bundles using (Func; _⟶ₛ_)
 open import Function.Base using (id; _∘_)
 open import Function.Construct.Setoid using (_∙_)
@@ -17,7 +19,7 @@ open import Functor.Instance.Nat.Push using (Push₁; Push-identity; Push-homomo
 open import Level using (suc)
 open import Relation.Binary.PropositionalEquality as ≡ using (_≗_)
 
-import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
+-- import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 import Function.Construct.Identity as Id
 
 open Func