Update push, pull, and sys functors

1 files changed, 71 insertions, 52 deletions

diff --git a/Functor/Instance/Nat/Pull.agda b/Functor/Instance/Nat/Pull.agda
index b1764d9..c2a06c6 100644
--- a/Functor/Instance/Nat/Pull.agda
+++ b/Functor/Instance/Nat/Pull.agda
@@ -2,80 +2,99 @@
 
 module Functor.Instance.Nat.Pull where
 
+open import Level using (0ℓ)
+
+open import Category.Instance.Setoids.SymmetricMonoidal {0ℓ} {0ℓ} using (Setoids-×)
+
 open import Categories.Category.Instance.Nat using (Natop)
-open import Categories.Category.Instance.Setoids using (Setoids)
 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.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.System.Values Monoid using (Values; _⊕_; module Object)
+open import Data.Unit using (⊤; tt)
 open import Function.Base using (id; _∘_)
-open import Function.Bundles using (Func; _⟶ₛ_)
+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 Object.Monoid.Commutative Setoids-×.symmetric using (CommutativeMonoid; CommutativeMonoid⇒)
 open import Relation.Binary using (Rel; Setoid)
 open import Relation.Binary.PropositionalEquality as ≡ using (_≗_)
-open import Data.Circuit.Value using (Monoid)
-open import Data.System.Values Monoid using (Values)
-open import Data.Unit using (⊤; tt)
 
+open CommutativeMonoid using (Carrier; monoid)
+open CommutativeMonoid⇒ using (arr)
 open Functor
 open Func
-
--- Pull takes a natural number n to the setoid Values n
+open Object using (Valuesₘ)
 
 private
 
   variable A B C : ℕ
 
-  _≈_ : {X Y : Setoid 0ℓ 0ℓ} → Rel (X ⟶ₛ Y) 0ℓ
-  _≈_ {X} {Y} = Setoid._≈_ (setoid X Y)
-
-  infixr 4 _≈_
-
-  opaque
+-- Pull takes a natural number n to the commutative monoid Valuesₘ n
 
-    unfolding Values
+Pull₀ : ℕ → CommutativeMonoid
+Pull₀ n = Valuesₘ n
 
-    -- 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
-
-    -- Pull respects identity
-    Pull-identity : Pull₁ id ≈ Id (Values A)
-    Pull-identity {A} = Setoid.refl (Values A)
-
-  opaque
-
-    unfolding Pull₁
-
-    -- 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
+-- action of Pull on morphisms (contravariant)
 
+-- setoid morphism
 opaque
+  unfolding Valuesₘ Values
+  Pullₛ : (Fin A → Fin B) → Carrier (Pull₀ B) ⟶ₛ Carrier (Pull₀ A)
+  Pullₛ f .to x = x ∘ f
+  Pullₛ f .cong x≗y = x≗y ∘ f
 
-  unfolding Pull₁
-
-  Pull-defs : ⊤
-  Pull-defs = tt
+-- monoid morphism
+opaque
+  unfolding _⊕_ Pullₛ
+  Pullₘ : (Fin A → Fin B) → CommutativeMonoid⇒ (Pull₀ B) (Pull₀ A)
+  Pullₘ {A} f = record
+      { monoid⇒ = record
+          { arr = Pullₛ f
+          ; preserves-μ = Setoid.refl (Values A)
+          ; preserves-η = Setoid.refl (Values A)
+          }
+      }
+
+-- Pull respects identity
+opaque
+  unfolding Pullₘ
+  Pull-identity
+      : (open Setoid (Carrier (Pull₀ A) ⇒ₛ Carrier (Pull₀ A)))
+      → arr (Pullₘ id) ≈ Id (Carrier (Pull₀ A))
+  Pull-identity {A} = Setoid.refl (Values A)
 
--- the Pull functor
-Pull : Functor Natop (Setoids 0ℓ 0ℓ)
-F₀ Pull = Values
-F₁ Pull = Pull₁
-identity Pull = Pull-identity
-homomorphism Pull {f = f} {g} = Pull-homomorphism g f
-F-resp-≈ Pull = Pull-resp-≈
+-- Pull flips composition
+opaque
+  unfolding Pullₘ
+  Pull-homomorphism
+      : (f : Fin A → Fin B)
+        (g : Fin B → Fin C)
+        (open Setoid (Carrier (Pull₀ C) ⇒ₛ Carrier (Pull₀ A)))
+      → arr (Pullₘ (g ∘ f)) ≈ arr (Pullₘ f) ∙ arr (Pullₘ g)
+  Pull-homomorphism {A} _ _ = Setoid.refl (Values A)
+
+-- Pull respects equality
+opaque
+  unfolding Pullₘ
+  Pull-resp-≈
+      : {f g : Fin A → Fin B}
+      → f ≗ g
+      → (open Setoid (Carrier (Pull₀ B) ⇒ₛ Carrier (Pull₀ A)))
+      → arr (Pullₘ f) ≈ arr (Pullₘ g)
+  Pull-resp-≈ f≗g {v} = ≡.cong v ∘ f≗g
+
+Pull : Functor Natop CMonoids
+Pull .F₀ = Pull₀
+Pull .F₁ = Pullₘ
+Pull .identity = Pull-identity
+Pull .homomorphism = Pull-homomorphism _ _
+Pull .F-resp-≈ = Pull-resp-≈
 
 module Pull = Functor Pull