Simplify System definition and add System functor

4 files changed, 107 insertions, 19 deletions

diff --git a/Data/System.agda b/Data/System.agda
index fa7d8e7..e2ac073 100644
--- a/Data/System.agda
+++ b/Data/System.agda
@@ -41,13 +41,13 @@ module _ {ℓ : Level} where
     field
       S : Setoid ℓ ℓ
       fₛ : ∣ Values n ⇒ₛ S ⇒ₛ S ∣
-      fₒ : ∣ Values n ⇒ₛ S ⇒ₛ Values n ∣
+      fₒ : ∣ S ⇒ₛ Values n ∣
 
     fₛ′ : ∣ Values n ∣ → ∣ S ∣ → ∣ S ∣
     fₛ′ = to ∘ to fₛ
 
-    fₒ′ : ∣ Values n ∣ → ∣ S ∣ → ∣ Values n ∣
-    fₒ′ = to ∘ to fₒ
+    fₒ′ : ∣ S ∣ → ∣ Values n ∣
+    fₒ′ = to fₒ
 
     open Setoid S public
 
@@ -62,15 +62,15 @@ module _ {ℓ : Level} where
             : (i : ∣ Values n ∣) (s : ∣ A.S ∣)
             → ⇒S ⟨$⟩ (A.fₛ′ i s) B.≈ B.fₛ′ i (⇒S ⟨$⟩ s)
         ≗-fₒ
-            : (i : ∣ Values n ∣) (s : ∣ A.S ∣)
-            → A.fₒ′ i s ≋ B.fₒ′ i (⇒S ⟨$⟩ s)
+            : (s : ∣ A.S ∣)
+            → A.fₒ′ s ≋ B.fₒ′ (⇒S ⟨$⟩ s)
 
     open ≤-System
 
     ≤-refl : Reflexive ≤-System
     ⇒S ≤-refl = Id.function _
-    ≗-fₛ (≤-refl {x}) p e = System.refl x
-    ≗-fₒ (≤-refl {x}) _ _ = ≋.refl
+    ≗-fₛ (≤-refl {x}) _ _ = System.refl x
+    ≗-fₒ (≤-refl {x}) _ = ≋.refl
 
     ≡⇒≤ : _≡_ ⇒ ≤-System
     ≡⇒≤ ≡.refl = ≤-refl
@@ -79,7 +79,7 @@ module _ {ℓ : Level} where
     ≤-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 {x} {y} {z} a b) i s = ≋.trans (≗-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
diff --git a/Functor/Instance/Nat/Pull.agda b/Functor/Instance/Nat/Pull.agda
index 3f13303..cf15809 100644
--- a/Functor/Instance/Nat/Pull.agda
+++ b/Functor/Instance/Nat/Pull.agda
@@ -7,12 +7,10 @@ open import Categories.Category.Instance.Nat using (Nat)
 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.Circuit.Value using (Value)
 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 Data.Vec.Functional.Relation.Binary.Equality.Setoid using (≋-setoid)
 open import Function.Base using (id; flip; _∘_)
 open import Function.Bundles using (Func; _⟶ₛ_)
 open import Function.Construct.Identity using () renaming (function to Id)
@@ -20,6 +18,7 @@ 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 Functor
 open Func
@@ -33,9 +32,7 @@ infixr 4 _≈_
 private
   variable A B C : ℕ
 
--- action on objects (Vector Value n)
-Values : ℕ → Setoid 0ℓ 0ℓ
-Values = ≋-setoid (≡.setoid Value)
+-- action on objects is Values n (Vector Value n)
 
 -- action of Pull on morphisms (contravariant)
 Pull₁ : (Fin A → Fin B) → Values B ⟶ₛ Values A
diff --git a/Functor/Instance/Nat/Push.agda b/Functor/Instance/Nat/Push.agda
index c7443ab..8b40bd7 100644
--- a/Functor/Instance/Nat/Push.agda
+++ b/Functor/Instance/Nat/Push.agda
@@ -5,20 +5,19 @@ module Functor.Instance.Nat.Push where
 open import Categories.Functor using (Functor)
 open import Categories.Category.Instance.Nat using (Nat)
 open import Categories.Category.Instance.Setoids using (Setoids)
-open import Data.Circuit.Value using (Value)
 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 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; _∙_)
 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 Func
 open Functor
@@ -30,9 +29,7 @@ _≈_ : {X Y : Setoid 0ℓ 0ℓ} → Rel (X ⟶ₛ Y) 0ℓ
 _≈_ {X} {Y} = Setoid._≈_ (setoid X Y)
 infixr 4 _≈_
 
--- action on objects (Vector Value n)
-Values : ℕ → Setoid 0ℓ 0ℓ
-Values = ≋-setoid (≡.setoid Value)
+-- 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
diff --git a/Functor/Instance/Nat/System.agda b/Functor/Instance/Nat/System.agda
new file mode 100644
index 0000000..2b96355
--- /dev/null
+++ b/Functor/Instance/Nat/System.agda
@@ -0,0 +1,94 @@
+{-# OPTIONS --without-K --safe #-}
+
+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.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 Function.Bundles using (Func; _⟶ₛ_)
+open import Function.Base using (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 Level using (suc)
+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
+
+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
+
+Sys : Functor Nat (Setoids (suc ℓ) ℓ)
+Sys .F₀ = Systemₛ
+Sys .F₁ = System₁
+Sys .identity = id-x≤x , x≤id-x
+Sys .homomorphism {x = X} = System-homomorphism {X = X}
+Sys .F-resp-≈ = System-resp-≈