Clean up System functors

3 files changed, 167 insertions, 120 deletions

diff --git a/Functor/Instance/Nat/Pull.agda b/Functor/Instance/Nat/Pull.agda
index 5b74399..b1764d9 100644
--- a/Functor/Instance/Nat/Pull.agda
+++ b/Functor/Instance/Nat/Pull.agda
@@ -14,50 +14,68 @@ 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.Circuit.Value using (Value)
-open import Data.System.Values Value using (Values)
+open import Data.Circuit.Value using (Monoid)
+open import Data.System.Values Monoid using (Values)
+open import Data.Unit using (⊤; tt)
 
 open Functor
 open Func
 
-_≈_ : {X Y : Setoid 0ℓ 0ℓ} → Rel (X ⟶ₛ Y) 0ℓ
-_≈_ {X} {Y} = Setoid._≈_ (setoid X Y)
-infixr 4 _≈_
+-- Pull takes a natural number n to the setoid Values n
 
 private
+
   variable A B C : ℕ
 
+  _≈_ : {X Y : Setoid 0ℓ 0ℓ} → Rel (X ⟶ₛ Y) 0ℓ
+  _≈_ {X} {Y} = Setoid._≈_ (setoid X Y)
+
+  infixr 4 _≈_
+
+  opaque
+
+    unfolding Values
+
+    -- action of Pull on morphisms (contravariant)
+    Pull₁ : (Fin A → Fin B) → Values B ⟶ₛ Values A
+    to (Pull₁ f) i = i ∘ f
+    cong (Pull₁ f) x≗y = x≗y ∘ f
 
--- action on objects is Values n (Vector Value n)
+    -- Pull respects identity
+    Pull-identity : Pull₁ id ≈ Id (Values A)
+    Pull-identity {A} = Setoid.refl (Values A)
 
--- action of Pull on morphisms (contravariant)
-Pull₁ : (Fin A → Fin B) → Values B ⟶ₛ Values A
-to (Pull₁ f) i = i ∘ f
-cong (Pull₁ f) x≗y = x≗y ∘ f
+  opaque
 
--- Pull respects identity
-Pull-identity : Pull₁ id ≈ Id (Values A)
-Pull-identity {A} = Setoid.refl (Values A)
+    unfolding Pull₁
 
--- Pull flips composition
-Pull-homomorphism
-    : {A B C : ℕ}
-      (f : Fin A → Fin B)
-      (g : Fin B → Fin C)
-    → Pull₁ (g ∘ f) ≈ Pull₁ f ∙ Pull₁ g
-Pull-homomorphism {A} _ _ = Setoid.refl (Values A)
+    -- Pull flips composition
+    Pull-homomorphism
+        : (f : Fin A → Fin B)
+          (g : Fin B → Fin C)
+        → Pull₁ (g ∘ f) ≈ Pull₁ f ∙ Pull₁ g
+    Pull-homomorphism {A} _ _ = Setoid.refl (Values A)
 
--- Pull respects equality
-Pull-resp-≈
-    : {f g : Fin A → Fin B}
-    → f ≗ g
-    → Pull₁ f ≈ Pull₁ g
-Pull-resp-≈ f≗g {v} = ≡.cong v ∘ f≗g
+    -- Pull respects equality
+    Pull-resp-≈
+        : {f g : Fin A → Fin B}
+        → f ≗ g
+        → Pull₁ f ≈ Pull₁ g
+    Pull-resp-≈ f≗g {v} = ≡.cong v ∘ f≗g
+
+opaque
+
+  unfolding Pull₁
+
+  Pull-defs : ⊤
+  Pull-defs = tt
 
 -- the Pull functor
 Pull : Functor Natop (Setoids 0ℓ 0ℓ)
 F₀ Pull = Values
 F₁ Pull = Pull₁
 identity Pull = Pull-identity
-homomorphism Pull {f = f} {g} {v} = Pull-homomorphism g f {v}
+homomorphism Pull {f = f} {g} = Pull-homomorphism g f
 F-resp-≈ Pull = Pull-resp-≈
+
+module Pull = Functor Pull
diff --git a/Functor/Instance/Nat/Push.agda b/Functor/Instance/Nat/Push.agda
index 53d0bef..8126006 100644
--- a/Functor/Instance/Nat/Push.agda
+++ b/Functor/Instance/Nat/Push.agda
@@ -17,43 +17,56 @@ 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.Circuit.Value using (Value)
-open import Data.System.Values Value using (Values)
+open import Data.Circuit.Value using (Monoid)
+open import Data.System.Values Monoid using (Values)
+open import Data.Unit using (⊤; tt)
 
 open Func
 open Functor
 
+-- Push sends a natural number n to Values n
+
 private
+
   variable A B C : ℕ
 
-_≈_ : {X Y : Setoid 0ℓ 0ℓ} → Rel (X ⟶ₛ Y) 0ℓ
-_≈_ {X} {Y} = Setoid._≈_ (setoid X Y)
-infixr 4 _≈_
+  _≈_ : {X Y : Setoid 0ℓ 0ℓ} → Rel (X ⟶ₛ Y) 0ℓ
+  _≈_ {X} {Y} = Setoid._≈_ (setoid X Y)
+  infixr 4 _≈_
+
+  opaque
+
+    unfolding Values
 
--- action of Push on objects is Values n (Vector Value n)
+    -- action of Push on morphisms (covariant)
+    Push₁ : (Fin A → Fin B) → Values A ⟶ₛ Values B
+    to (Push₁ f) v = merge v ∘ preimage f ∘ ⁅_⁆
+    cong (Push₁ f) x≗y = merge-cong₁ x≗y ∘ preimage f ∘ ⁅_⁆
 
--- action of Push on morphisms (covariant)
-Push₁ : (Fin A → Fin B) → Values A ⟶ₛ Values B
-to (Push₁ f) v = merge v ∘ preimage f ∘ ⁅_⁆
-cong (Push₁ f) x≗y = merge-cong₁ x≗y ∘ preimage f ∘ ⁅_⁆
+    -- Push respects identity
+    Push-identity : Push₁ id ≈ Id (Values A)
+    Push-identity {_} {v} = merge-⁅⁆ v
 
--- Push respects identity
-Push-identity : Push₁ id ≈ Id (Values A)
-Push-identity {_} {v} = merge-⁅⁆ v
+    -- Push respects composition
+    Push-homomorphism
+        : {f : Fin A → Fin B}
+          {g : Fin B → Fin C}
+        → Push₁ (g ∘ f) ≈ Push₁ g ∙ Push₁ f
+    Push-homomorphism {f = f} {g} {v} = merge-preimage f v ∘ preimage g ∘ ⁅_⁆
 
--- Push respects composition
-Push-homomorphism
-    : {f : Fin A → Fin B}
-      {g : Fin B → Fin C}
-    → Push₁ (g ∘ f) ≈ Push₁ g ∙ Push₁ f
-Push-homomorphism {f = f} {g} {v} = merge-preimage f v ∘ preimage g ∘ ⁅_⁆
+    -- Push respects equality
+    Push-resp-≈
+        : {f g : Fin A → Fin B}
+        → f ≗ g
+        → Push₁ f ≈ Push₁ g
+    Push-resp-≈ f≗g {v} = merge-cong₂ v ∘ preimage-cong₁ f≗g ∘ ⁅_⁆
 
--- Push respects equality
-Push-resp-≈
-    : {f g : Fin A → Fin B}
-    → f ≗ g
-    → Push₁ f ≈ Push₁ g
-Push-resp-≈ f≗g {v} = merge-cong₂ v ∘ preimage-cong₁ f≗g ∘ ⁅_⁆
+opaque
+
+  unfolding Push₁
+
+  Push-defs : ⊤
+  Push-defs = tt
 
 -- the Push functor
 Push : Functor Nat (Setoids 0ℓ 0ℓ)
@@ -62,3 +75,5 @@ F₁ Push = Push₁
 identity Push = Push-identity
 homomorphism Push = Push-homomorphism
 F-resp-≈ Push = Push-resp-≈
+
+module Push = Functor Push
diff --git a/Functor/Instance/Nat/System.agda b/Functor/Instance/Nat/System.agda
index 00451ad..05e1e7b 100644
--- a/Functor/Instance/Nat/System.agda
+++ b/Functor/Instance/Nat/System.agda
@@ -2,91 +2,103 @@
 
 module Functor.Instance.Nat.System where
 
+
 open import Level using (suc; 0ℓ)
+
 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.Circuit.Value using (Monoid)
 open import Data.Fin.Base using (Fin)
 open import Data.Nat.Base using (ℕ)
 open import Data.Product.Base using (_,_; _×_)
-open import Data.System {suc 0ℓ} using (System; ≤-System; Systemₛ)
-open import Data.System.Values Value using (module ≋)
-open import Function.Bundles using (Func; _⟶ₛ_)
+open import Data.System {suc 0ℓ} using (System; _≤_; Systemₛ)
+open import Data.System.Values Monoid using (module ≋)
+open import Data.Unit using (⊤; tt)
 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 (_∙_)
-open import Functor.Instance.Nat.Pull using (Pull₁; Pull-resp-≈)
-open import Functor.Instance.Nat.Push using (Push₁; Push-identity; Push-homomorphism; Push-resp-≈)
+open import Functor.Instance.Nat.Pull using (Pull)
+open import Functor.Instance.Nat.Push using (Push)
 open import Relation.Binary.PropositionalEquality as ≡ using (_≗_)
 
--- import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
-import Function.Construct.Identity as Id
-
 open Func
-open ≤-System
 open Functor
+open _≤_
 
 private
+
   variable A B C : ℕ
 
-map : (Fin A → Fin B) → System A → System B
-map f X = record
-    { S = S
-    ; fₛ = fₛ ∙ Pull₁ f
-    ; fₒ = Push₁ f ∙ fₒ
-    }
-  where
-    open System X
-
-≤-cong : (f : Fin A → Fin B) {X Y : System A} → ≤-System Y X → ≤-System (map f Y) (map f X)
-⇒S (≤-cong f x≤y) = ⇒S x≤y
-≗-fₛ (≤-cong f x≤y) = ≗-fₛ x≤y ∘ to (Pull₁ f)
-≗-fₒ (≤-cong f x≤y) = cong (Push₁ f) ∘ ≗-fₒ x≤y
-
-System₁ : (Fin A → Fin B) → Systemₛ A ⟶ₛ Systemₛ B
-to (System₁ f) = map f
-cong (System₁ f) (x≤y , y≤x) = ≤-cong f x≤y , ≤-cong f y≤x
-
-id-x≤x : {X : System A} → ≤-System (map id X) X
-⇒S (id-x≤x) = Id.function _
-≗-fₛ (id-x≤x {_} {x}) i s = System.refl x
-≗-fₒ (id-x≤x {A} {x}) s = Push-identity
-
-x≤id-x : {x : System A} → ≤-System x (map id x)
-⇒S x≤id-x = Id.function _
-≗-fₛ (x≤id-x {A} {x}) i s = System.refl x
-≗-fₒ (x≤id-x {A} {x}) s = ≋.sym Push-identity
-
-
-System-homomorphism
-    : {f : Fin A → Fin B}
-      {g : Fin B → Fin C} 
-      {X : System A}
-    → ≤-System (map (g ∘ f) X) (map g (map f X)) × ≤-System (map g (map f X)) (map (g ∘ f) X)
-System-homomorphism {f = f} {g} {X} = left , right
-  where
-    open System X
-    left : ≤-System (map (g ∘ f) X) (map g (map f X))
-    left .⇒S = Id.function S
-    left .≗-fₛ i s = refl
-    left .≗-fₒ s = Push-homomorphism
-    right : ≤-System (map g (map f X)) (map (g ∘ f) X)
-    right .⇒S = Id.function S
-    right .≗-fₛ i s = refl
-    right .≗-fₒ s = ≋.sym Push-homomorphism
-
-System-resp-≈
-    : {f g : Fin A → Fin B}
-    → f ≗ g
-    → {X : System A}
-    → (≤-System (map f X) (map g X)) × (≤-System (map g X) (map f X))
-System-resp-≈ {A} {B} {f = f} {g} f≗g {X} = both f≗g , both (≡.sym ∘ f≗g)
-  where
-    open System X
-    both : {f g : Fin A → Fin B} → f ≗ g → ≤-System (map f X) (map g X)
-    both f≗g .⇒S = Id.function S
-    both f≗g .≗-fₛ i s = cong fₛ (Pull-resp-≈ f≗g {i})
-    both {f} {g} f≗g .≗-fₒ s = Push-resp-≈ f≗g
+  opaque
+
+    map : (Fin A → Fin B) → System A → System B
+    map f X = let open System X in record
+        { S = S
+        ; fₛ = fₛ ∙ Pull.₁ f
+        ; fₒ = Push.₁ f ∙ fₒ
+        }
+
+    ≤-cong : (f : Fin A → Fin B) {X Y : System A} → Y ≤ X → map f Y ≤ map f X
+    ⇒S (≤-cong f x≤y) = ⇒S x≤y
+    ≗-fₛ (≤-cong f x≤y) = ≗-fₛ x≤y ∘ to (Pull.₁ f)
+    ≗-fₒ (≤-cong f x≤y) = cong (Push.₁ f) ∘ ≗-fₒ x≤y
+
+    System₁ : (Fin A → Fin B) → Systemₛ A ⟶ₛ Systemₛ B
+    to (System₁ f) = map f
+    cong (System₁ f) (x≤y , y≤x) = ≤-cong f x≤y , ≤-cong f y≤x
+
+  opaque
+
+    unfolding System₁
+
+    id-x≤x : {X : System A} → System₁ id ⟨$⟩ X ≤ X
+    ⇒S (id-x≤x) = Id _
+    ≗-fₛ (id-x≤x {_} {x}) i s = cong (System.fₛ x) Pull.identity
+    ≗-fₒ (id-x≤x {A} {x}) s = Push.identity
+
+    x≤id-x : {x : System A} → x ≤ System₁ id ⟨$⟩ x
+    ⇒S x≤id-x = Id _
+    ≗-fₛ (x≤id-x {A} {x}) i s = cong (System.fₛ x) (≋.sym Pull.identity)
+    ≗-fₒ (x≤id-x {A} {x}) s = ≋.sym Push.identity
+
+    System-homomorphism
+        : {f : Fin A → Fin B}
+          {g : Fin B → Fin C} 
+          {X : System A}
+        → System₁ (g ∘ f) ⟨$⟩ X ≤ System₁ g ⟨$⟩ (System₁ f ⟨$⟩ X)
+        × System₁ g ⟨$⟩ (System₁ f ⟨$⟩ X) ≤ System₁ (g ∘ f) ⟨$⟩ X
+    System-homomorphism {f = f} {g} {X} = left , right
+      where
+        open System X
+        left : map (g ∘ f) X ≤ map g (map f X)
+        left .⇒S = Id S
+        left .≗-fₛ i s = cong fₛ Pull.homomorphism
+        left .≗-fₒ s = Push.homomorphism
+        right : map g (map f X) ≤ map (g ∘ f) X
+        right .⇒S = Id S
+        right .≗-fₛ i s = cong fₛ (≋.sym Pull.homomorphism)
+        right .≗-fₒ s = ≋.sym Push.homomorphism
+
+    System-resp-≈
+        : {f g : Fin A → Fin B}
+        → f ≗ g
+        → {X : System A}
+        → System₁ f ⟨$⟩ X ≤ System₁ g ⟨$⟩ X
+        × System₁ g ⟨$⟩ X ≤ System₁ f ⟨$⟩ X
+    System-resp-≈ {A} {B} {f = f} {g} f≗g {X} = both f≗g , both (≡.sym ∘ f≗g)
+      where
+        open System X
+        both : {f g : Fin A → Fin B} → f ≗ g → map f X ≤ map g X
+        both f≗g .⇒S = Id S
+        both f≗g .≗-fₛ i s = cong fₛ (Pull.F-resp-≈ f≗g {i})
+        both {f} {g} f≗g .≗-fₒ s = Push.F-resp-≈ f≗g
+
+opaque
+  unfolding System₁
+  Sys-defs : ⊤
+  Sys-defs = tt
 
 Sys : Functor Nat (Setoids (suc 0ℓ) (suc 0ℓ))
 Sys .F₀ = Systemₛ
@@ -94,3 +106,5 @@ Sys .F₁ = System₁
 Sys .identity = id-x≤x , x≤id-x
 Sys .homomorphism {x = X} = System-homomorphism {X = X}
 Sys .F-resp-≈ = System-resp-≈
+
+module Sys = Functor Sys