Split System into smaller modules

7 files changed, 111 insertions, 100 deletions

diff --git a/Data/Setoid.agda b/Data/Setoid.agda
new file mode 100644
index 0000000..454d276
--- /dev/null
+++ b/Data/Setoid.agda
@@ -0,0 +1,8 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Setoid where
+
+open import Relation.Binary using (Setoid)
+open import Function.Construct.Setoid using () renaming (setoid to infixr 0 _⇒ₛ_) public
+
+open Setoid renaming (Carrier to ∣_∣) public
diff --git a/Data/System.agda b/Data/System.agda
index e2ac073..0361369 100644
--- a/Data/System.agda
+++ b/Data/System.agda
@@ -1,100 +1,86 @@
 {-# OPTIONS --without-K --safe #-}
 
-module Data.System where
+open import Level using (Level)
 
+module Data.System {ℓ : Level} where
+
+import Function.Construct.Identity as Id
 import Relation.Binary.Properties.Preorder as PreorderProperties
 
 open import Data.Circuit.Value using (Value)
 open import Data.Nat.Base using (ℕ)
-open import Data.Vec.Functional using (Vector)
+open import Data.Setoid using (_⇒ₛ_; ∣_∣)
+open import Data.System.Values Value using (Values; _≋_; module ≋)
 open import Level using (Level; _⊔_; 0ℓ; suc)
 open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
-open import Relation.Binary using (Rel; Reflexive; Transitive; Preorder; _⇒_; Setoid)
-open import Function.Base using (id; _∘_)
-import Function.Construct.Identity as Id
-open import Data.Vec.Functional.Relation.Binary.Equality.Setoid using (≋-setoid)
+open import Relation.Binary using (Reflexive; Transitive; Preorder; _⇒_; Setoid)
+open import Function.Base using (_∘_)
+open import Function.Bundles using (Func; _⟨$⟩_)
+open import Function.Construct.Setoid using (_∙_)
 
-open import Function.Bundles using (Func; _⟶ₛ_; _⟨$⟩_)
-
-open import Function.Construct.Setoid using (setoid; _∙_)
 open Func
 
-_⇒ₛ_ : {a₁ a₂ b₁ b₂ : Level} → Setoid a₁ a₂ → Setoid b₁ b₂ → Setoid (a₁ ⊔ a₂ ⊔ b₁ ⊔ b₂) (a₁ ⊔ b₂)
-_⇒ₛ_ = setoid
-
-infixr 0 _⇒ₛ_
+record System (n : ℕ) : Set (suc ℓ) where
 
-∣_∣ : {c ℓ : Level} → Setoid c ℓ → Set c
-∣_∣ = Setoid.Carrier
+  field
+    S : Setoid ℓ ℓ
+    fₛ : ∣ Values n ⇒ₛ S ⇒ₛ S ∣
+    fₒ : ∣ S ⇒ₛ Values n ∣
 
-Values : ℕ → Setoid 0ℓ 0ℓ
-Values = ≋-setoid (≡.setoid Value)
+  fₛ′ : ∣ Values n ∣ → ∣ S ∣ → ∣ S ∣
+  fₛ′ = to ∘ to fₛ
 
-_≋_ : {n : ℕ} → Rel (Vector Value n) 0ℓ
-_≋_ {n} = Setoid._≈_ (Values n)
+  fₒ′ : ∣ S ∣ → ∣ Values n ∣
+  fₒ′ = to fₒ
 
-module ≋ {n : ℕ} = Setoid (Values n)
+  open Setoid S public
 
-module _ {ℓ : Level} where
+module _ {n : ℕ} where
 
-  record System (n : ℕ) : Set (suc ℓ) where
+  record ≤-System (a b : System n) : Set ℓ where
+    module A = System a
+    module B = System b
     field
-      S : Setoid ℓ ℓ
-      fₛ : ∣ Values n ⇒ₛ S ⇒ₛ S ∣
-      fₒ : ∣ S ⇒ₛ Values n ∣
-
-    fₛ′ : ∣ Values n ∣ → ∣ S ∣ → ∣ S ∣
-    fₛ′ = to ∘ to fₛ
-
-    fₒ′ : ∣ S ∣ → ∣ Values n ∣
-    fₒ′ = to fₒ
-
-    open Setoid S public
-
-  module _ {n : ℕ} where
-
-    record ≤-System (a b : System n) : Set ℓ where
-      module A = System a
-      module B = System b
-      field
-        ⇒S : ∣ A.S ⇒ₛ B.S ∣
-        ≗-fₛ
-            : (i : ∣ Values n ∣) (s : ∣ A.S ∣)
-            → ⇒S ⟨$⟩ (A.fₛ′ i s) B.≈ B.fₛ′ i (⇒S ⟨$⟩ s)
-        ≗-fₒ
-            : (s : ∣ A.S ∣)
-            → A.fₒ′ s ≋ B.fₒ′ (⇒S ⟨$⟩ s)
-
-    open ≤-System
-
-    ≤-refl : Reflexive ≤-System
-    ⇒S ≤-refl = Id.function _
-    ≗-fₛ (≤-refl {x}) _ _ = System.refl x
-    ≗-fₒ (≤-refl {x}) _ = ≋.refl
-
-    ≡⇒≤ : _≡_ ⇒ ≤-System
-    ≡⇒≤ ≡.refl = ≤-refl
-
-    open System
-    ≤-trans : Transitive ≤-System
-    ⇒S (≤-trans a b) = ⇒S b ∙ ⇒S a
-    ≗-fₛ (≤-trans {x} {y} {z} a b) i s = System.trans z (cong (⇒S b) (≗-fₛ a i s)) (≗-fₛ b i (⇒S a ⟨$⟩ s))
-    ≗-fₒ (≤-trans a b) s = ≋.trans (≗-fₒ a s) (≗-fₒ b (⇒S a ⟨$⟩ s))
-
-    System-Preorder : Preorder (suc ℓ) (suc ℓ) ℓ
-    System-Preorder = record
-        { Carrier = System n
-        ; _≈_ = _≡_
-        ; _≲_ = ≤-System
-        ; isPreorder = record
-            { isEquivalence = ≡.isEquivalence
-            ; reflexive = ≡⇒≤
-            ; trans = ≤-trans
-            }
-        }
-
-  module _ (n : ℕ) where
-
-    open PreorderProperties (System-Preorder {n}) using (InducedEquivalence)
-    Systemₛ : Setoid (suc ℓ) ℓ
-    Systemₛ = InducedEquivalence
+      ⇒S : ∣ A.S ⇒ₛ B.S ∣
+      ≗-fₛ
+          : (i : ∣ Values n ∣) (s : ∣ A.S ∣)
+          → ⇒S ⟨$⟩ (A.fₛ′ i s) B.≈ B.fₛ′ i (⇒S ⟨$⟩ s)
+      ≗-fₒ
+          : (s : ∣ A.S ∣)
+          → A.fₒ′ s ≋ B.fₒ′ (⇒S ⟨$⟩ s)
+
+  open ≤-System
+
+  ≤-refl : Reflexive ≤-System
+  ⇒S ≤-refl = Id.function _
+  ≗-fₛ (≤-refl {x}) _ _ = System.refl x
+  ≗-fₒ (≤-refl {x}) _ = ≋.refl
+
+  ≡⇒≤ : _≡_ ⇒ ≤-System
+  ≡⇒≤ ≡.refl = ≤-refl
+
+  open System
+
+  ≤-trans : Transitive ≤-System
+  ⇒S (≤-trans a b) = ⇒S b ∙ ⇒S a
+  ≗-fₛ (≤-trans {x} {y} {z} a b) i s = System.trans z (cong (⇒S b) (≗-fₛ a i s)) (≗-fₛ b i (⇒S a ⟨$⟩ s))
+  ≗-fₒ (≤-trans a b) s = ≋.trans (≗-fₒ a s) (≗-fₒ b (⇒S a ⟨$⟩ s))
+
+  System-Preorder : Preorder (suc ℓ) (suc ℓ) ℓ
+  System-Preorder = record
+      { Carrier = System n
+      ; _≈_ = _≡_
+      ; _≲_ = ≤-System
+      ; isPreorder = record
+          { isEquivalence = ≡.isEquivalence
+          ; reflexive = ≡⇒≤
+          ; trans = ≤-trans
+          }
+      }
+
+module _ (n : ℕ) where
+
+  open PreorderProperties (System-Preorder {n}) using (InducedEquivalence)
+
+  Systemₛ : Setoid (suc ℓ) ℓ
+  Systemₛ = InducedEquivalence
diff --git a/Data/System/Values.agda b/Data/System/Values.agda
new file mode 100644
index 0000000..bf8fa38
--- /dev/null
+++ b/Data/System/Values.agda
@@ -0,0 +1,21 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Data.System.Values (A : Set) where
+
+open import Data.Nat.Base using (ℕ)
+open import Data.Vec.Functional using (Vector)
+open import Level using (0ℓ)
+open import Relation.Binary using (Rel; Setoid)
+open import Data.Vec.Functional.Relation.Binary.Equality.Setoid using (≋-setoid)
+
+import Relation.Binary.PropositionalEquality as ≡
+
+Values : ℕ → Setoid 0ℓ 0ℓ
+Values = ≋-setoid (≡.setoid A)
+
+_≋_ : {n : ℕ} → Rel (Vector A n) 0ℓ
+_≋_ {n} = Setoid._≈_ (Values n)
+
+infix 4 _≋_
+
+module ≋ {n : ℕ} = Setoid (Values n)
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