Update push, pull, and sys functors

7 files changed, 892 insertions, 290 deletions

diff --git a/Data/CMonoid.agda b/Data/CMonoid.agda
index 8aaf869..dd0277c 100644
--- a/Data/CMonoid.agda
+++ b/Data/CMonoid.agda
@@ -3,19 +3,16 @@
 open import Level using (Level)
 module Data.CMonoid {c ℓ : Level} where
 
-open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory)
+import Algebra.Bundles as Alg
+
+open import Algebra.Morphism using (IsMonoidHomomorphism)
+open import Categories.Object.Monoid using (Monoid)
 open import Category.Instance.Setoids.SymmetricMonoidal {c} {ℓ} using (Setoids-×; ×-symmetric′)
+open import Data.Monoid {c} {ℓ} using (toMonoid; fromMonoid; toMonoid⇒; module FromMonoid)
+open import Data.Product using (_,_; Σ)
+open import Function using (Func; _⟨$⟩_; _⟶ₛ_)
 open import Object.Monoid.Commutative using (CommutativeMonoid; CommutativeMonoid⇒)
-open import Categories.Object.Monoid using (Monoid)
-
-open import Data.Monoid {c} {ℓ} using (toMonoid; fromMonoid; toMonoid⇒)
 
-import Algebra.Bundles as Alg
-
-open import Data.Setoid using (∣_∣)
-open import Relation.Binary using (Setoid)
-open import Function using (Func; _⟨$⟩_)
-open import Data.Product using (curry′; uncurry′; _,_)
 open Func
 
 -- A commutative monoid object in the (symmetric monoidal) category of setoids
@@ -37,9 +34,6 @@ toCMonoid M = record
       comm : (x y : M.Carrier) → x M.∙ y M.≈ y M.∙ x
       comm x y = commutative {x , y}
 
-open import Function.Construct.Constant using () renaming (function to Const)
-open import Data.Setoid.Unit using (⊤ₛ)
-
 fromCMonoid : Alg.CommutativeMonoid c ℓ → CommutativeMonoid Setoids-×.symmetric
 fromCMonoid M = record
     { M
@@ -53,7 +47,7 @@ fromCMonoid M = record
     module M = Monoid (fromMonoid monoid)
     open Setoids-× using (_≈_; _∘_; module braiding)
     opaque
-      unfolding toMonoid
+      unfolding FromMonoid.μ
       commutative : M.μ ≈ M.μ ∘ braiding.⇒.η _
       commutative {x , y} = comm x y
 
@@ -64,9 +58,6 @@ module  _ (M N : CommutativeMonoid Setoids-×.symmetric) where
   module M = Alg.CommutativeMonoid (toCMonoid M)
   module N = Alg.CommutativeMonoid (toCMonoid N)
 
-  open import Data.Product using (Σ; _,_)
-  open import Function using (_⟶ₛ_)
-  open import Algebra.Morphism using (IsMonoidHomomorphism)
   open CommutativeMonoid
   open CommutativeMonoid⇒
 
diff --git a/Data/Monoid.agda b/Data/Monoid.agda
index 1ba0af4..02a8062 100644
--- a/Data/Monoid.agda
+++ b/Data/Monoid.agda
@@ -1,25 +1,26 @@
 {-# OPTIONS --without-K --safe #-}
 
 open import Level using (Level)
-module Data.Monoid {c ℓ : Level} where
 
-open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory)
-open import Category.Instance.Setoids.SymmetricMonoidal {c} {ℓ} using (Setoids-×; ×-monoidal′)
-open import Categories.Object.Monoid using (Monoid; Monoid⇒)
+module Data.Monoid {c ℓ : Level} where
 
 import Algebra.Bundles as Alg
 
+open import Algebra.Morphism using (IsMonoidHomomorphism)
+open import Categories.Object.Monoid using (Monoid; Monoid⇒)
+open import Category.Instance.Setoids.SymmetricMonoidal {c} {ℓ} using (Setoids-×; ×-monoidal′)
+open import Data.Product using (curry′; uncurry′; _,_; Σ)
 open import Data.Setoid using (∣_∣)
+open import Data.Setoid.Unit using (⊤ₛ)
+open import Function using (Func; _⟶ₛ_; _⟨$⟩_)
+open import Function.Construct.Constant using () renaming (function to Const)
+open import Function.Construct.Identity using () renaming (function to Id)
 open import Relation.Binary using (Setoid)
-open import Function using (Func)
-open import Data.Product using (curry′; uncurry′; _,_)
+
 open Func
 
 -- A monoid object in the (monoidal) category of setoids is just a monoid
 
-open import Function.Construct.Constant using () renaming (function to Const)
-open import Data.Setoid.Unit using (⊤ₛ)
-
 opaque
   unfolding ×-monoidal′
   toMonoid : Monoid Setoids-×.monoidal → Alg.Monoid c ℓ
@@ -43,19 +44,57 @@ opaque
       open Monoid M renaming (Carrier to A)
       open Setoid A
 
-  fromMonoid : Alg.Monoid c ℓ → Monoid Setoids-×.monoidal
-  fromMonoid M = record
+module FromMonoid (M : Alg.Monoid c ℓ) where
+
+  open Alg.Monoid M
+  open Setoids-× using (_⊗₁_; _⊗₀_; _∘_; unit; module unitorˡ; module unitorʳ; module associator)
+
+  opaque
+
+    unfolding ×-monoidal′
+
+    μ : setoid ⊗₀ setoid ⟶ₛ setoid
+    μ .to = uncurry′ _∙_
+    μ .cong = uncurry′ ∙-cong
+
+    η : unit ⟶ₛ setoid
+    η = Const ⊤ₛ setoid ε
+
+  opaque
+
+    unfolding μ
+
+    μ-assoc
+        : {x : ∣ (setoid ⊗₀ setoid) ⊗₀ setoid ∣}
+        → μ ∘ μ ⊗₁ Id setoid ⟨$⟩ x
+        ≈ μ ∘ Id setoid ⊗₁ μ ∘ associator.from ⟨$⟩ x
+    μ-assoc {(x , y) , z} = assoc x y z
+
+    μ-identityˡ
+        : {x : ∣ unit ⊗₀ setoid ∣}
+        → unitorˡ.from ⟨$⟩ x
+        ≈ μ ∘ η ⊗₁ Id setoid ⟨$⟩ x
+    μ-identityˡ {_ , x} = sym (identityˡ x)
+
+    μ-identityʳ
+        : {x : ∣ setoid ⊗₀ unit ∣}
+        → unitorʳ.from ⟨$⟩ x
+        ≈ μ ∘ Id setoid ⊗₁ η ⟨$⟩ x
+    μ-identityʳ {x , _} = sym (identityʳ x)
+
+  fromMonoid : Monoid Setoids-×.monoidal
+  fromMonoid = record
       { Carrier = setoid
       ; isMonoid = record
-          { μ = record { to = uncurry′ _∙_ ; cong = uncurry′ ∙-cong }
-          ; η = Const ⊤ₛ setoid ε
-          ; assoc = λ { {(x , y) , z} → assoc x y z }
-          ; identityˡ = λ { {_ , x} → sym (identityˡ x) }
-          ; identityʳ = λ { {x , _} → sym (identityʳ x) }
+          { μ = μ
+          ; η = η
+          ; assoc = μ-assoc
+          ; identityˡ = μ-identityˡ
+          ; identityʳ = μ-identityʳ
           }
       }
-    where
-      open Alg.Monoid M
+
+open FromMonoid using (fromMonoid) public
 
 -- A morphism of monoids in the (monoidal) category of setoids is a monoid homomorphism
 
@@ -64,9 +103,6 @@ module  _ (M N : Monoid Setoids-×.monoidal) where
   module M = Alg.Monoid (toMonoid M)
   module N = Alg.Monoid (toMonoid N)
 
-  open import Data.Product using (Σ; _,_)
-  open import Function using (_⟶ₛ_)
-  open import Algebra.Morphism using (IsMonoidHomomorphism)
   open Monoid⇒
 
   opaque
diff --git a/Data/System.agda b/Data/System.agda
index d71c2a8..d12fa12 100644
--- a/Data/System.agda
+++ b/Data/System.agda
@@ -66,53 +66,51 @@ module _ {n : ℕ} where
 
 open System
 
-private
-
-  module _ {n : ℕ} where
-
-    open _≤_
-
-    ≤-refl : Reflexive (_≤_ {n})
-    ⇒S ≤-refl = Id _
-    ≗-fₛ (≤-refl {x}) _ _ = S.refl x
-    ≗-fₒ ≤-refl _ = ≋.refl
-
-    ≡⇒≤ : _≡_ Rel.⇒ _≤_
-    ≡⇒≤ ≡.refl = ≤-refl
-
-    ≤-trans : Transitive _≤_
-    ⇒S (≤-trans a b) = ⇒S b ∙ ⇒S a
-    ≗-fₛ (≤-trans {x} {y} {z} a b) i s = let open ≈-Reasoning (S z) in begin
-        ⇒S b ⟨$⟩ (⇒S a ⟨$⟩ (fₛ′ x i s)) ≈⟨ cong (⇒S b) (≗-fₛ a i s) ⟩
-        ⇒S b ⟨$⟩ (fₛ′ y i (⇒S a ⟨$⟩ s)) ≈⟨ ≗-fₛ b i (⇒S a ⟨$⟩ s) ⟩
-        fₛ′ z i (⇒S b ⟨$⟩ (⇒S a ⟨$⟩ s)) ∎
-    ≗-fₒ (≤-trans {x} {y} {z} a b) s = let open ≈-Reasoning (Values n) in begin
-        fₒ′ x s                       ≈⟨ ≗-fₒ a s ⟩
-        fₒ′ y (⇒S a ⟨$⟩ s)            ≈⟨ ≗-fₒ b (⇒S a ⟨$⟩ s) ⟩
-        fₒ′ z (⇒S b ⟨$⟩ (⇒S a ⟨$⟩ s)) ∎
-
-    variable
-      A B C : System n
-
-    _≈_ : Rel (A ≤ B) 0ℓ
-    _≈_ {A} {B} ≤₁ ≤₂ = ⇒S ≤₁ A⇒B.≈ ⇒S ≤₂
-      where
-        module A⇒B = Setoid (S A ⇒ₛ S B)
-
-    open Rel.IsEquivalence
-
-    ≈-isEquiv : Rel.IsEquivalence (_≈_ {A} {B})
-    ≈-isEquiv {B = B} .refl = S.refl B
-    ≈-isEquiv {B = B} .sym a = S.sym B a
-    ≈-isEquiv {B = B} .trans a b = S.trans B a b
-
-    ≤-resp-≈ : {f h : B ≤ C} {g i : A ≤ B} → f ≈ h → g ≈ i → ≤-trans g f ≈ ≤-trans i h
-    ≤-resp-≈ {_} {C} {_} {f} {h} {g} {i} f≈h g≈i {x} = begin
-        ⇒S f ⟨$⟩ (⇒S g ⟨$⟩ x) ≈⟨ f≈h ⟩
-        ⇒S h ⟨$⟩ (⇒S g ⟨$⟩ x) ≈⟨ cong (⇒S h) g≈i ⟩
-        ⇒S h ⟨$⟩ (⇒S i ⟨$⟩ x) ∎
-      where
-        open ≈-Reasoning (System.S C)
+module _ {n : ℕ} where
+
+  open _≤_
+
+  ≤-refl : Reflexive (_≤_ {n})
+  ⇒S ≤-refl = Id _
+  ≗-fₛ (≤-refl {x}) _ _ = S.refl x
+  ≗-fₒ ≤-refl _ = ≋.refl
+
+  ≡⇒≤ : _≡_ Rel.⇒ _≤_
+  ≡⇒≤ ≡.refl = ≤-refl
+
+  ≤-trans : Transitive _≤_
+  ⇒S (≤-trans a b) = ⇒S b ∙ ⇒S a
+  ≗-fₛ (≤-trans {x} {y} {z} a b) i s = let open ≈-Reasoning (S z) in begin
+      ⇒S b ⟨$⟩ (⇒S a ⟨$⟩ (fₛ′ x i s)) ≈⟨ cong (⇒S b) (≗-fₛ a i s) ⟩
+      ⇒S b ⟨$⟩ (fₛ′ y i (⇒S a ⟨$⟩ s)) ≈⟨ ≗-fₛ b i (⇒S a ⟨$⟩ s) ⟩
+      fₛ′ z i (⇒S b ⟨$⟩ (⇒S a ⟨$⟩ s)) ∎
+  ≗-fₒ (≤-trans {x} {y} {z} a b) s = let open ≈-Reasoning (Values n) in begin
+      fₒ′ x s                       ≈⟨ ≗-fₒ a s ⟩
+      fₒ′ y (⇒S a ⟨$⟩ s)            ≈⟨ ≗-fₒ b (⇒S a ⟨$⟩ s) ⟩
+      fₒ′ z (⇒S b ⟨$⟩ (⇒S a ⟨$⟩ s)) ∎
+
+  variable
+    A B C : System n
+
+  _≈_ : Rel (A ≤ B) 0ℓ
+  _≈_ {A} {B} ≤₁ ≤₂ = ⇒S ≤₁ A⇒B.≈ ⇒S ≤₂
+    where
+      module A⇒B = Setoid (S A ⇒ₛ S B)
+
+  open Rel.IsEquivalence
+
+  ≈-isEquiv : Rel.IsEquivalence (_≈_ {A} {B})
+  ≈-isEquiv {B = B} .refl = S.refl B
+  ≈-isEquiv {B = B} .sym a = S.sym B a
+  ≈-isEquiv {B = B} .trans a b = S.trans B a b
+
+  ≤-resp-≈ : {f h : B ≤ C} {g i : A ≤ B} → f ≈ h → g ≈ i → ≤-trans g f ≈ ≤-trans i h
+  ≤-resp-≈ {_} {C} {_} {f} {h} {g} {i} f≈h g≈i {x} = begin
+      ⇒S f ⟨$⟩ (⇒S g ⟨$⟩ x) ≈⟨ f≈h ⟩
+      ⇒S h ⟨$⟩ (⇒S g ⟨$⟩ x) ≈⟨ cong (⇒S h) g≈i ⟩
+      ⇒S h ⟨$⟩ (⇒S i ⟨$⟩ x) ∎
+    where
+      open ≈-Reasoning (System.S C)
 
 System-≤ : ℕ → Preorder (suc 0ℓ) (suc 0ℓ) ℓ
 System-≤ n = record
diff --git a/Data/System/Values.agda b/Data/System/Values.agda
index 545a835..d1cd6c9 100644
--- a/Data/System/Values.agda
+++ b/Data/System/Values.agda
@@ -5,53 +5,98 @@ open import Level using (0ℓ)
 
 module Data.System.Values (A : CommutativeMonoid 0ℓ 0ℓ) where
 
-import Algebra.Properties.CommutativeMonoid.Sum as Sum
-import Data.Vec.Functional.Relation.Binary.Equality.Setoid as Pointwise
-import Relation.Binary.PropositionalEquality as ≡
+open import Category.Instance.Setoids.SymmetricMonoidal {0ℓ} {0ℓ} using (Setoids-×)
 
-open import Data.Fin using (_↑ˡ_; _↑ʳ_; zero; suc; splitAt)
-open import Data.Nat using (ℕ; _+_; suc)
-open import Data.Product using (_,_)
+import Algebra.Properties.CommutativeMonoid.Sum A as Sum
+import Data.Vec.Functional.Relation.Binary.Equality.Setoid as Pointwise
+import Object.Monoid.Commutative Setoids-×.symmetric as Obj
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
+
+open import Data.Bool using (Bool; if_then_else_)
+open import Data.Bool.Properties using (if-cong)
+open import Data.Monoid using (module FromMonoid)
+open import Data.CMonoid using (fromCMonoid)
+open import Data.Fin using (Fin; splitAt; _↑ˡ_; _↑ʳ_; punchIn; punchOut)
+open import Data.Fin using (_≟_)
+open import Data.Fin.Permutation using (Permutation; Permutation′; _⟨$⟩ʳ_; _⟨$⟩ˡ_; id; flip; inverseˡ; inverseʳ; punchIn-permute; insert; remove)
+open import Data.Fin.Preimage using (preimage; preimage-cong₁; preimage-cong₂)
+open import Data.Fin.Properties using (punchIn-punchOut)
+open import Data.Nat using (ℕ; _+_)
+open import Data.Product using (_,_; Σ-syntax)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
 open import Data.Setoid using (∣_∣)
+open import Data.Subset.Functional using (Subset; ⁅_⁆; ⁅⁆∘ρ)
 open import Data.Sum using (inj₁; inj₂)
 open import Data.Vec.Functional as Vec using (Vector; zipWith; replicate)
 open import Function using (Func; _⟶ₛ_; _⟨$⟩_; _∘_)
 open import Level using (0ℓ)
 open import Relation.Binary using (Rel; Setoid; IsEquivalence)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_; module ≡-Reasoning)
+open import Relation.Nullary.Decidable using (yes; no)
 
-open CommutativeMonoid A renaming (Carrier to Value)
+open Bool
+open CommutativeMonoid A renaming (Carrier to Value; setoid to Valueₛ)
+open Fin
 open Func
-open Sum A using (sum)
-
-open Pointwise setoid using (≋-setoid; ≋-isEquivalence)
+open Pointwise Valueₛ using (≋-setoid; ≋-isEquivalence)
+open ℕ
 
 opaque
-
   Values : ℕ → Setoid 0ℓ 0ℓ
   Values = ≋-setoid
 
+_when_ : Value → Bool → Value
+x when b = if b then x else ε
+
+-- when preserves setoid equivalence
+when-cong
+    : {x y : Value}
+    → x ≈ y
+    → (b : Bool)
+    → x when b ≈ y when b
+when-cong _ false = refl
+when-cong x≈y true = x≈y
+
 module _ {n : ℕ} where
 
   opaque
 
     unfolding Values
 
-    merge : ∣ Values n ∣ → Value
-    merge = sum
-
     _⊕_ : ∣ Values n ∣ → ∣ Values n ∣ → ∣ Values n ∣
     xs ⊕ ys = zipWith _∙_ xs ys
 
     <ε> : ∣ Values n ∣
     <ε> = replicate n ε
 
+    mask : Subset n → ∣ Values n ∣ → ∣ Values n ∣
+    mask S v i = v i when S i
+
+    sum : ∣ Values n ∣ → Value
+    sum = Sum.sum
+
+    merge : ∣ Values n ∣ → Subset n → Value
+    merge v S = sum (mask S v)
+
+    -- mask preserves setoid equivalence
+    maskₛ : Subset n → Values n ⟶ₛ Values n
+    maskₛ S .to = mask S
+    maskₛ S .cong v≋w i = when-cong (v≋w i) (S i)
+
+    -- sum preserves setoid equivalence
+    sumₛ : Values n ⟶ₛ Valueₛ
+    sumₛ .to = Sum.sum
+    sumₛ .cong = Sum.sum-cong-≋
+
     head : ∣ Values (suc n) ∣ → Value
     head xs = xs zero
 
     tail : ∣ Values (suc n) ∣ → ∣ Values n ∣
     tail xs = xs ∘ suc
 
+    lookup : ∣ Values n ∣ → Fin n → Value
+    lookup v i = v i
+
   module ≋ = Setoid (Values n)
 
   _≋_ : Rel ∣ Values n ∣ 0ℓ
@@ -59,16 +104,45 @@ module _ {n : ℕ} where
 
   infix 4 _≋_
 
-opaque
+  opaque
+
+    unfolding merge
+
+    -- merge preserves setoid equivalence
+    merge-cong
+        : (S : Subset n)
+        → {xs ys : ∣ Values n ∣}
+        → xs ≋ ys
+        → merge xs S ≈ merge ys S
+    merge-cong S {xs} {ys} xs≋ys = cong sumₛ (cong (maskₛ S) xs≋ys)
+
+    mask-cong₁
+        : {S₁ S₂ : Subset n}
+        → S₁ ≗ S₂
+        → (xs : ∣ Values n ∣)
+        → mask S₁ xs ≋ mask S₂ xs
+    mask-cong₁ S₁≋S₂ _ i = reflexive (if-cong (S₁≋S₂ i))
+
+    merge-cong₂
+        : (xs : ∣ Values n ∣)
+        → {S₁ S₂ : Subset n}
+        → S₁ ≗ S₂
+        → merge xs S₁ ≈ merge xs S₂
+    merge-cong₂ xs S₁≋S₂ = cong sumₛ (mask-cong₁ S₁≋S₂ xs)
+
+module _ where
 
-  unfolding Values
   open Setoid
-  ≋-isEquiv : ∀ n → IsEquivalence (_≈_ (Values n))
-  ≋-isEquiv = ≋-isEquivalence
+
+  opaque
+    unfolding Values
+    ≋-isEquiv : ∀ n → IsEquivalence (_≈_ (Values n))
+    ≋-isEquiv = ≋-isEquivalence
 
 module _ {n : ℕ} where
 
   opaque
+
     unfolding _⊕_
 
     ⊕-cong : {x y u v : ≋.Carrier {n}} → x ≋ y → u ≋ v → x ⊕ u ≋ y ⊕ v
@@ -86,25 +160,35 @@ module _ {n : ℕ} where
     ⊕-comm : (x y : ≋.Carrier {n}) → x ⊕ y ≋ y ⊕ x
     ⊕-comm x y i = comm (x i) (y i)
 
-open CommutativeMonoid
-Valuesₘ : ℕ → CommutativeMonoid 0ℓ 0ℓ
-Valuesₘ n .Carrier = ∣ Values n ∣
-Valuesₘ n ._≈_ = _≋_
-Valuesₘ n ._∙_ = _⊕_
-Valuesₘ n .ε = <ε>
-Valuesₘ n .isCommutativeMonoid = record
-    { isMonoid = record
-        { isSemigroup = record
-            { isMagma = record
-                { isEquivalence = ≋-isEquiv n
-                ; ∙-cong = ⊕-cong
-                }
-            ; assoc = ⊕-assoc
-            }
-        ; identity = ⊕-identityˡ , ⊕-identityʳ
-        }
-    ; comm = ⊕-comm
-    }
+module Algebra where
+
+  open CommutativeMonoid
+
+  Valuesₘ : ℕ → CommutativeMonoid 0ℓ 0ℓ
+  Valuesₘ n .Carrier = ∣ Values n ∣
+  Valuesₘ n ._≈_ = _≋_
+  Valuesₘ n ._∙_ = _⊕_
+  Valuesₘ n .ε = <ε>
+  Valuesₘ n .isCommutativeMonoid = record
+      { isMonoid = record
+          { isSemigroup = record
+              { isMagma = record
+                  { isEquivalence = ≋-isEquiv n
+                  ; ∙-cong = ⊕-cong
+                  }
+              ; assoc = ⊕-assoc
+              }
+          ; identity = ⊕-identityˡ , ⊕-identityʳ
+          }
+      ; comm = ⊕-comm
+      }
+
+module Object where
+
+  opaque
+    unfolding FromMonoid.μ
+    Valuesₘ : ℕ → Obj.CommutativeMonoid
+    Valuesₘ n = fromCMonoid (Algebra.Valuesₘ n)
 
 opaque
 
@@ -144,3 +228,290 @@ module _ {n m : ℕ} where
   ++ₛ : Values n ×ₛ Values m ⟶ₛ Values (n + m)
   to ++ₛ (xs , ys) = xs ++ ys
   cong ++ₛ (≗xs , ≗ys) = ++-cong _ _ ≗xs ≗ys
+
+opaque
+
+  unfolding merge
+
+  mask-⊕
+      : {n : ℕ}
+        (xs ys : ∣ Values n ∣)
+        (S : Subset n)
+      → mask S (xs ⊕ ys) ≋ mask S xs ⊕ mask S ys
+  mask-⊕ xs ys S i with S i
+  ... | false = sym (identityˡ ε)
+  ... | true = refl
+
+  sum-⊕
+      : {n : ℕ}
+      → (xs ys : ∣ Values n ∣)
+      → sum (xs ⊕ ys) ≈ sum xs ∙ sum ys
+  sum-⊕ {zero} xs ys = sym (identityˡ ε)
+  sum-⊕ {suc n} xs ys = begin
+      (head xs ∙ head ys) ∙ sum (tail xs ⊕ tail ys)         ≈⟨ ∙-congˡ (sum-⊕ (tail xs) (tail ys)) ⟩
+      (head xs ∙ head ys) ∙ (sum (tail xs) ∙ sum (tail ys)) ≈⟨ assoc (head xs) (head ys) _ ⟩
+      head xs ∙ (head ys ∙ (sum (tail xs) ∙ sum (tail ys))) ≈⟨ ∙-congˡ (assoc (head ys) (sum (tail xs)) _) ⟨
+      head xs ∙ ((head ys ∙ sum (tail xs)) ∙ sum (tail ys)) ≈⟨ ∙-congˡ (∙-congʳ (comm (head ys) (sum (tail xs)))) ⟩
+      head xs ∙ ((sum (tail xs) ∙ head ys) ∙ sum (tail ys)) ≈⟨ ∙-congˡ (assoc (sum (tail xs)) (head ys) _) ⟩
+      head xs ∙ (sum (tail xs) ∙ (head ys ∙ sum (tail ys))) ≈⟨ assoc (head xs) (sum (tail xs)) _ ⟨
+      (head xs ∙ sum (tail xs)) ∙ (head ys ∙ sum (tail ys)) ∎
+    where
+      open ≈-Reasoning Valueₛ
+
+  merge-⊕
+      : {n : ℕ}
+        (xs ys : ∣ Values n ∣)
+        (S : Subset n)
+      → merge (xs ⊕ ys) S ≈ merge xs S ∙ merge ys S
+  merge-⊕ {n} xs ys S = begin
+      sum (mask S (xs ⊕ ys))            ≈⟨ cong sumₛ (mask-⊕ xs ys S) ⟩
+      sum (mask S xs ⊕ mask S ys)       ≈⟨ sum-⊕ (mask S xs) (mask S ys) ⟩
+      sum (mask S xs) ∙ sum (mask S ys) ∎
+    where
+      open ≈-Reasoning Valueₛ
+
+  mask-<ε> : {n : ℕ} (S : Subset n) → mask {n} S <ε> ≋ <ε>
+  mask-<ε> S i with S i
+  ... | false = refl
+  ... | true = refl
+
+  sum-<ε> : (n : ℕ) → sum {n} <ε> ≈ ε
+  sum-<ε> zero = refl
+  sum-<ε> (suc n) = trans (identityˡ (sum {n} <ε>)) (sum-<ε> n)
+
+  merge-<ε> : {n : ℕ} (S : Subset n) → merge {n} <ε> S ≈ ε
+  merge-<ε> {n} S = begin
+      sum (mask S <ε>)  ≈⟨ cong sumₛ (mask-<ε> S) ⟩
+      sum {n} <ε>       ≈⟨ sum-<ε> n ⟩
+      ε                 ∎
+    where
+      open ≈-Reasoning Valueₛ
+
+  merge-⁅⁆
+      : {n : ℕ}
+        (xs : ∣ Values n ∣)
+        (i : Fin n)
+      → merge xs ⁅ i ⁆ ≈ lookup xs i
+  merge-⁅⁆ {suc n} xs zero = trans (∙-congˡ (sum-<ε> n)) (identityʳ (head xs))
+  merge-⁅⁆ {suc n} xs (suc i) = begin
+      ε ∙ merge (tail xs) ⁅ i ⁆ ≈⟨ identityˡ (sum (mask ⁅ i ⁆ (tail xs))) ⟩
+      merge (tail xs) ⁅ i ⁆     ≈⟨ merge-⁅⁆ (tail xs) i ⟩
+      tail xs i                 ∎
+    where
+      open ≈-Reasoning Valueₛ
+
+opaque
+
+  unfolding Values
+
+  push : {A B : ℕ} → ∣ Values A ∣ → (Fin A → Fin B) → ∣ Values B ∣
+  push v f = merge v ∘ preimage f ∘ ⁅_⁆
+
+  pull : {A B : ℕ} → ∣ Values B ∣ → (Fin A → Fin B) → ∣ Values A ∣
+  pull v f = v ∘ f
+
+insert-f0-0
+    : {A B : ℕ}
+      (f : Fin (suc A) → Fin (suc B))
+    → Σ[ ρ ∈ Permutation′ (suc B) ] (ρ ⟨$⟩ʳ (f zero) ≡ zero)
+insert-f0-0 {A} {B} f = ρ , ρf0≡0
+  where
+    ρ : Permutation′ (suc B)
+    ρ = insert (f zero) zero id
+    ρf0≡0 : ρ ⟨$⟩ʳ f zero ≡ zero
+    ρf0≡0 with f zero ≟ f zero
+    ... | yes _ = ≡.refl
+    ... | no f0≢f0 with () ← f0≢f0 ≡.refl
+
+opaque
+  unfolding push
+  push-cong
+      : {A B : ℕ}
+      → (v : ∣ Values A ∣)
+        {f g : Fin A → Fin B}
+      → f ≗ g
+      → push v f ≋ push v g
+  push-cong v f≋g i = merge-cong₂ v (≡.cong ⁅ i ⁆ ∘ f≋g)
+
+opaque
+  unfolding Values
+  removeAt : {n : ℕ} → ∣ Values (suc n) ∣ → Fin (suc n) → ∣ Values n ∣
+  removeAt v i = Vec.removeAt v i
+
+opaque
+  unfolding merge removeAt
+  merge-removeAt
+      : {A : ℕ}
+        (k : Fin (suc A))
+        (v : ∣ Values (suc A) ∣)
+        (S : Subset (suc A))
+      → merge v S ≈ lookup v k when S k ∙ merge (removeAt v k) (Vec.removeAt S k)
+  merge-removeAt {A} zero v S = refl
+  merge-removeAt {suc A} (suc k) v S = begin
+      v0? ∙ merge (tail v) (Vec.tail S)           ≈⟨ ∙-congˡ (merge-removeAt k (tail v) (Vec.tail S)) ⟩
+      v0? ∙ (vk? ∙ merge (tail v-) (Vec.tail S-)) ≈⟨ assoc v0? vk? _ ⟨
+      (v0? ∙ vk?) ∙ merge (tail v-) (Vec.tail S-) ≈⟨ ∙-congʳ (comm v0? vk?) ⟩
+      (vk? ∙ v0?) ∙ merge (tail v-) (Vec.tail S-) ≈⟨ assoc vk? v0? _ ⟩
+      vk? ∙ (v0? ∙ merge (tail v-) (Vec.tail S-)) ≡⟨⟩
+      vk? ∙ merge v- S- ∎
+    where
+      open ≈-Reasoning Valueₛ
+      v0? vk? : Value
+      v0? = head v when Vec.head S
+      vk? = tail v k when Vec.tail S k
+      v- : Vector Value (suc A)
+      v- = removeAt v (suc k)
+      S- : Subset (suc A)
+      S- = Vec.removeAt S (suc k)
+
+opaque
+  unfolding merge pull removeAt
+  merge-preimage-ρ
+      : {A B : ℕ}
+      → (ρ : Permutation A B)
+      → (v : ∣ Values A ∣)
+        (S : Subset B)
+      → merge v (preimage (ρ ⟨$⟩ʳ_) S) ≈ merge (pull v (ρ ⟨$⟩ˡ_)) S
+  merge-preimage-ρ {zero} {zero} ρ v S = refl
+  merge-preimage-ρ {zero} {suc B} ρ v S with () ← ρ ⟨$⟩ˡ zero
+  merge-preimage-ρ {suc A} {zero} ρ v S with () ← ρ ⟨$⟩ʳ zero
+  merge-preimage-ρ {suc A} {suc B} ρ v S = begin
+      merge v (preimage ρʳ S)                                       ≈⟨ merge-removeAt (ρˡ zero) v (preimage ρʳ S) ⟩
+      mask (preimage ρʳ S) v (ρˡ zero) ∙ merge v- [preimage-ρʳ-S]-  ≈⟨ ∙-congʳ ≈vρˡ0? ⟩
+      mask S (pull v ρˡ) zero ∙ merge v- [preimage-ρʳ-S]-           ≈⟨ ∙-congˡ (merge-cong₂ v- preimage-) ⟩
+      mask S (pull v ρˡ) zero ∙ merge v- (preimage ρʳ- S-)          ≈⟨ ∙-congˡ (merge-preimage-ρ ρ- v- S-) ⟩
+      mask S (pull v ρˡ) zero ∙ merge (pull v- ρˡ-) S-              ≈⟨ ∙-congˡ (merge-cong S- (reflexive ∘ pull-v-ρˡ-)) ⟩
+      mask S (pull v ρˡ) zero ∙ merge (tail (pull v ρˡ)) S-         ≡⟨⟩
+      merge (pull v ρˡ) S                                           ∎
+    where
+      ρˡ : Fin (suc B) → Fin (suc A)
+      ρˡ = ρ ⟨$⟩ˡ_
+      ρʳ : Fin (suc A) → Fin (suc B)
+      ρʳ = ρ ⟨$⟩ʳ_
+      ρ- : Permutation A B
+      ρ- = remove (ρˡ zero) ρ
+      ρˡ- : Fin B → Fin A
+      ρˡ- = ρ- ⟨$⟩ˡ_
+      ρʳ- : Fin A → Fin B
+      ρʳ- = ρ- ⟨$⟩ʳ_
+      v- : ∣ Values A ∣
+      v- = removeAt v (ρˡ zero)
+      S- : Subset B
+      S- = S ∘ suc
+      [preimage-ρʳ-S]- : Subset A
+      [preimage-ρʳ-S]- = Vec.removeAt (preimage ρʳ S) (ρˡ zero)
+      vρˡ0? : Value
+      vρˡ0? = head (pull v ρˡ) when S zero
+      ≈vρˡ0?  : mask (S ∘ ρʳ ∘ ρˡ) (pull v ρˡ) zero ≈ mask S (pull v ρˡ) zero
+      ≈vρˡ0? = mask-cong₁ (λ i → ≡.cong S (inverseʳ ρ {i})) (pull v ρˡ) zero
+      module _ where
+        open ≡-Reasoning
+        preimage- : [preimage-ρʳ-S]- ≗ preimage ρʳ- S-
+        preimage- x = begin
+            [preimage-ρʳ-S]- x                        ≡⟨⟩
+            Vec.removeAt (preimage ρʳ S) (ρˡ zero) x  ≡⟨⟩
+            S (ρʳ (punchIn (ρˡ zero) x))              ≡⟨ ≡.cong S (punchIn-permute ρ (ρˡ zero) x) ⟩ 
+            S (punchIn (ρʳ (ρˡ zero)) (ρʳ- x))        ≡⟨ ≡.cong (λ h → S (punchIn h (ρʳ- x))) (inverseʳ ρ) ⟩ 
+            S (punchIn zero (ρʳ- x))                  ≡⟨⟩ 
+            S (suc (ρʳ- x))                           ≡⟨⟩
+            preimage ρʳ- S- x                         ∎
+        pull-v-ρˡ- : pull v- ρˡ- ≗ tail (pull v ρˡ)
+        pull-v-ρˡ- i = begin
+            v- (ρˡ- i)                                        ≡⟨⟩
+            v (punchIn (ρˡ zero) (punchOut {A} {ρˡ zero} _))  ≡⟨ ≡.cong v (punchIn-punchOut _) ⟩
+            v (ρˡ (punchIn (ρʳ (ρˡ zero)) i))                 ≡⟨ ≡.cong (λ h → v (ρˡ (punchIn h i))) (inverseʳ ρ) ⟩
+            v (ρˡ (punchIn zero i))                           ≡⟨⟩
+            v (ρˡ (suc i))                                    ≡⟨⟩
+            tail (v ∘ ρˡ) i                                   ∎
+      open ≈-Reasoning Valueₛ
+
+opaque
+
+  unfolding push merge mask
+
+  mutual
+
+    merge-preimage
+        : {A B : ℕ}
+          (f : Fin A → Fin B)
+        → (v : ∣ Values A ∣)
+          (S : Subset B)
+        → merge v (preimage f S) ≈ merge (push v f) S
+    merge-preimage {zero} {zero} f v S = refl
+    merge-preimage {zero} {suc B} f v S = sym (trans (cong sumₛ (mask-<ε> S)) (sum-<ε> (suc B)))
+    merge-preimage {suc A} {zero} f v S with () ← f zero
+    merge-preimage {suc A} {suc B} f v S with insert-f0-0 f
+    ... | ρ , ρf0≡0 = begin
+            merge v (preimage f S)                      ≈⟨ merge-cong₂ v (preimage-cong₁ (λ x → inverseˡ ρ {f x}) S) ⟨
+            merge v (preimage (ρˡ ∘ ρʳ ∘ f) S)          ≡⟨⟩
+            merge v (preimage (ρʳ ∘ f) (preimage ρˡ S)) ≈⟨ merge-preimage-f0≡0 (ρʳ ∘ f) ρf0≡0 v (preimage ρˡ S) ⟩
+            merge (push v (ρʳ ∘ f)) (preimage ρˡ S)     ≈⟨ merge-preimage-ρ (flip ρ) (push v (ρʳ ∘ f)) S ⟩
+            merge (pull (push v (ρʳ ∘ f)) ρʳ) S         ≈⟨ merge-cong S (merge-cong₂ v ∘ preimage-cong₂ (ρʳ ∘ f) ∘ ⁅⁆∘ρ ρ) ⟩
+            merge (push v (ρˡ ∘ ρʳ ∘ f)) S              ≈⟨ merge-cong S (push-cong v (λ x → inverseˡ ρ {f x})) ⟩
+            merge (push v f) S      ∎
+          where
+            open ≈-Reasoning Valueₛ
+            ρʳ ρˡ : Fin (ℕ.suc B) → Fin (ℕ.suc B)
+            ρʳ = ρ ⟨$⟩ʳ_
+            ρˡ = ρ ⟨$⟩ˡ_
+
+    merge-preimage-f0≡0
+        : {A B : ℕ}
+          (f : Fin (suc A) → Fin (suc B))
+        → f zero ≡ zero
+        → (v : ∣ Values (suc A) ∣)
+          (S : Subset (suc B))
+        → merge v (preimage f S) ≈ merge (push v f) S
+    merge-preimage-f0≡0 {A} {B} f f0≡0 v S
+      using S0 , S- ← S zero , S ∘ suc
+      using v0 , v- ← head v , tail v
+      using f0 , f- ← f zero , f ∘ suc = begin
+          merge v f⁻¹[S]                    ≡⟨⟩
+          v0? ∙ merge v- f⁻¹[S]-            ≈⟨ ∙-congˡ (merge-preimage f- v- S) ⟩
+          v0? ∙ merge f[v-] S               ≡⟨⟩
+          v0? ∙ (f[v-]0? ∙ merge f[v-]- S-) ≈⟨ assoc v0? f[v-]0? (merge f[v-]- S-) ⟨
+          v0? ∙ f[v-]0? ∙ merge f[v-]- S-   ≈⟨ ∙-congʳ v0?∙f[v-]0?≈f[v]0? ⟩
+          f[v]0? ∙ merge f[v-]- S-          ≈⟨ ∙-congˡ (merge-cong S- ≋f[v]-) ⟩
+          f[v]0? ∙ merge f[v]- S-           ≡⟨⟩
+          merge f[v] S                      ∎
+        where
+          open ≈-Reasoning Valueₛ
+          f⁻¹[S] : Subset (suc A)
+          f⁻¹[S] = preimage f S
+          f⁻¹[S]- : Subset A
+          f⁻¹[S]- = f⁻¹[S] ∘ suc
+          f⁻¹[S]0 : Bool
+          f⁻¹[S]0 = f⁻¹[S] zero
+          f[v] : ∣ Values (suc B) ∣
+          f[v] = push v f
+          f[v]- : Vector Value B
+          f[v]- = tail f[v]
+          f[v]0 : Value
+          f[v]0 = head f[v]
+          f[v-] : ∣ Values (suc B) ∣
+          f[v-] = push v- f-
+          f[v-]- : Vector Value B
+          f[v-]- = tail f[v-]
+          f[v-]0 : Value
+          f[v-]0 = head f[v-]
+          v0? f[v-]0? v0?+[f[v-]0?] f[v]0? : Value
+          v0? = v0 when f⁻¹[S]0
+          f[v-]0? = f[v-]0 when S0
+          v0?+[f[v-]0?] = if S0 then v0? ∙ f[v-]0 else v0?
+          f[v]0? = f[v]0 when S0
+          v0?∙f[v-]0?≈f[v]0? : v0? ∙ f[v-]0? ≈ f[v]0?
+          v0?∙f[v-]0?≈f[v]0? rewrite f0≡0 with S0
+          ... | true = refl
+          ... | false = identityˡ ε
+          ≋f[v]- : f[v-]- ≋ f[v]-
+          ≋f[v]- x rewrite f0≡0 = sym (identityˡ (push v- f- (suc x)))
+
+opaque
+  unfolding push
+  merge-push
+      : {A B C : ℕ}
+        (f : Fin A → Fin B)
+        (g : Fin B → Fin C)
+      → (v : ∣ Values A ∣)
+      → push v (g ∘ f) ≋ push (push v f) g
+  merge-push f g v i = merge-preimage f v (preimage g ⁅ i ⁆)
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
diff --git a/Functor/Instance/Nat/Push.agda b/Functor/Instance/Nat/Push.agda
index 8126006..71b9a63 100644
--- a/Functor/Instance/Nat/Push.agda
+++ b/Functor/Instance/Nat/Push.agda
@@ -2,78 +2,115 @@
 
 module Functor.Instance.Nat.Push where
 
-open import Categories.Functor using (Functor)
+open import Level using (0ℓ)
+open import Category.Instance.Setoids.SymmetricMonoidal {0ℓ} {0ℓ} using (Setoids-×)
+
 open import Categories.Category.Instance.Nat using (Nat)
 open import Categories.Category.Instance.Setoids using (Setoids)
-open import Data.Circuit.Merge using (merge; merge-cong₁; merge-cong₂; merge-⁅⁆; merge-preimage)
-open import Data.Fin.Base using (Fin)
+open import Categories.Functor using (Functor)
+open import Category.Construction.CMonoids Setoids-×.symmetric using (CMonoids)
+open import Data.Circuit.Value using (Monoid)
+open import Data.Fin using (Fin)
 open import Data.Fin.Preimage using (preimage; preimage-cong₁)
-open import Data.Nat.Base using (ℕ)
+open import Data.Nat using (ℕ)
+open import Data.Setoid using (∣_∣; _⇒ₛ_)
 open import Data.Subset.Functional using (⁅_⁆)
-open import Function.Base using (id; _∘_)
-open import Function.Bundles using (Func; _⟶ₛ_)
+open import Data.System.Values Monoid using (Values; module Object; _⊕_; <ε>; _≋_; ≋-isEquiv; merge; push; merge-⊕; merge-<ε>; merge-cong; merge-⁅⁆; merge-push; merge-cong₂)
+open import Function using (Func; _⟶ₛ_; _⟨$⟩_; _∘_; id)
 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 Function.Construct.Setoid using (_∙_)
+open import Object.Monoid.Commutative Setoids-×.symmetric using (CommutativeMonoid; CommutativeMonoid⇒)
+open import Relation.Binary using (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 Func
 open Functor
-
--- Push sends a natural number n to 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 _≈_
+  -- Push sends a natural number n to Values n
+  Push₀ : ℕ → CommutativeMonoid
+  Push₀ n = Valuesₘ n
+
+  -- action of Push on morphisms (covariant)
 
   opaque
 
     unfolding Values
 
-    -- 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 ∘ ⁅_⁆
+    open CommutativeMonoid using (Carrier)
+    open CommutativeMonoid⇒ using (arr)
+
+    -- setoid morphism
+    Pushₛ : (Fin A → Fin B) → Values A ⟶ₛ Values B
+    Pushₛ f .to v = merge v ∘ preimage f ∘ ⁅_⁆
+    Pushₛ f .cong x≗y i = merge-cong (preimage f ⁅ i ⁆) x≗y
+
+  opaque
+
+    unfolding Pushₛ _⊕_
+
+    Push-⊕
+        : (f : Fin A → Fin B)
+        → (xs ys : ∣ Values A ∣)
+        → Pushₛ f ⟨$⟩ (xs ⊕ ys)
+        ≋ (Pushₛ f ⟨$⟩ xs) ⊕ (Pushₛ f ⟨$⟩ ys)
+    Push-⊕ f xs ys i = merge-⊕ xs ys (preimage f ⁅ i ⁆)
+
+    Push-<ε>
+        : (f : Fin A → Fin B)
+        → Pushₛ f ⟨$⟩ <ε> ≋ <ε>
+    Push-<ε> f i = merge-<ε> (preimage f ⁅ i ⁆)
+
+  opaque
+
+    unfolding Push-⊕ ≋-isEquiv Valuesₘ
+
+    -- monoid morphism
+    Pushₘ : (Fin A → Fin B) → CommutativeMonoid⇒ (Valuesₘ A) (Valuesₘ B)
+    Pushₘ f = record
+        { monoid⇒ = record
+            { arr = Pushₛ f
+            ; preserves-μ = Push-⊕ f _ _
+            ; preserves-η = Push-<ε> f
+            }
+        }
 
     -- Push respects identity
-    Push-identity : Push₁ id ≈ Id (Values A)
-    Push-identity {_} {v} = merge-⁅⁆ v
+    Push-identity
+      : (open Setoid (Carrier (Push₀ A) ⇒ₛ Carrier (Push₀ A)))
+      → arr (Pushₘ id) ≈ Id (Carrier (Push₀ A))
+    Push-identity {_} {v} i = merge-⁅⁆ v i
+
+  opaque
+
+    unfolding Pushₘ push
 
     -- 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 ∘ ⁅_⁆
+        → (open Setoid (Carrier (Push₀ A) ⇒ₛ Carrier (Push₀ C)))
+        → arr (Pushₘ (g ∘ f)) ≈ arr (Pushₘ g) ∙ arr (Pushₘ f)
+    Push-homomorphism {f = f} {g} {v} = merge-push f g v
 
     -- Push respects equality
     Push-resp-≈
         : {f g : Fin A → Fin B}
         → f ≗ g
-        → Push₁ f ≈ Push₁ g
+        → (open Setoid (Carrier (Push₀ A) ⇒ₛ Carrier (Push₀ B)))
+        → arr (Pushₘ f) ≈ arr (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ℓ)
-F₀ Push = Values
-F₁ Push = Push₁
-identity Push = Push-identity
-homomorphism Push = Push-homomorphism
-F-resp-≈ Push = Push-resp-≈
+Push : Functor Nat CMonoids
+Push .F₀ = Push₀
+Push .F₁ = Pushₘ
+Push .identity = Push-identity
+Push .homomorphism = Push-homomorphism
+Push .F-resp-≈ = Push-resp-≈
 
 module Push = Functor Push
diff --git a/Functor/Instance/Nat/System.agda b/Functor/Instance/Nat/System.agda
index 05e1e7b..4a651f2 100644
--- a/Functor/Instance/Nat/System.agda
+++ b/Functor/Instance/Nat/System.agda
@@ -1,110 +1,260 @@
 {-# OPTIONS --without-K --safe #-}
+{-# OPTIONS --hidden-argument-puns #-}
 
 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 Categories.Category using (Category)
+open import Categories.Category.Instance.Cats using (Cats)
+open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; niHelper)
+open import Categories.Functor using (Functor; _∘F_) renaming (id to idF)
 open import Data.Circuit.Value using (Monoid)
-open import Data.Fin.Base using (Fin)
-open import Data.Nat.Base using (ℕ)
+open import Data.Fin using (Fin)
+open import Data.Nat using (ℕ)
 open import Data.Product.Base using (_,_; _×_)
-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 Data.Setoid using (∣_∣)
+open import Data.System {suc 0ℓ} using (System; _≤_; Systemₛ; Systems; ≤-refl; ≤-trans; _≈_)
+open import Data.System.Values Monoid using (module ≋; module Object; Values; ≋-isEquiv)
+open import Relation.Binary using (Setoid)
+open import Function using (Func; _⟶ₛ_; _⟨$⟩_; _∘_; id)
 open import Function.Construct.Identity using () renaming (function to Id)
 open import Function.Construct.Setoid using (_∙_)
 open import Functor.Instance.Nat.Pull using (Pull)
 open import Functor.Instance.Nat.Push using (Push)
 open import Relation.Binary.PropositionalEquality as ≡ using (_≗_)
 
+open import Category.Instance.Setoids.SymmetricMonoidal {0ℓ} {0ℓ} using (Setoids-×)
+open import Category.Construction.CMonoids Setoids-×.symmetric using (CMonoids)
+open import Object.Monoid.Commutative Setoids-×.symmetric using (CommutativeMonoid; CommutativeMonoid⇒)
+
+open CommutativeMonoid⇒ using (arr)
+open Object using (Valuesₘ)
 open Func
 open Functor
 open _≤_
 
 private
-
   variable A B C : ℕ
 
-  opaque
+opaque
+  unfolding Valuesₘ ≋-isEquiv
+  map : (Fin A → Fin B) → System A → System B
+  map {A} {B} f X = let open System X in record
+      { S = S
+      ; fₛ = fₛ ∙ arr (Pull.₁ f)
+      ; fₒ = arr (Push.₁ f) ∙ fₒ
+      }
+
+opaque
+  unfolding map
+  open System
+  map-≤ : (f : Fin A → Fin B) {X Y : System A} → X ≤ Y → map f X ≤ map f Y
+  ⇒S (map-≤ f x≤y) = ⇒S x≤y
+  ≗-fₛ (map-≤ f x≤y) = ≗-fₛ x≤y ∘ to (arr (Pull.₁ f))
+  ≗-fₒ (map-≤ f x≤y) = cong (arr (Push.₁ f)) ∘ ≗-fₒ x≤y
+
+opaque
+  unfolding map-≤
+  map-≤-refl
+      : (f : Fin A → Fin B)
+      → {X : System A}
+      → map-≤ f (≤-refl {A} {X}) ≈ ≤-refl
+  map-≤-refl f {X} = Setoid.refl (S (map f X))
+
+opaque
+  unfolding map-≤
+  map-≤-trans
+      : (f : Fin A → Fin B)
+      → {X Y Z : System A}
+      → {h : X ≤ Y}
+      → {g : Y ≤ Z}
+      → map-≤ f (≤-trans h g) ≈ ≤-trans (map-≤ f h) (map-≤ f g)
+  map-≤-trans f {Z = Z} = Setoid.refl (S (map f Z))
 
-    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ₒ
+opaque
+  unfolding map-≤
+  map-≈
+      : (f : Fin A → Fin B)
+      → {X Y : System A}
+      → {g h : X ≤ Y}
+      → h ≈ g
+      → map-≤ f h ≈ map-≤ f g
+  map-≈ f h≈g = h≈g
+
+Sys₁ : (Fin A → Fin B) → Functor (Systems A) (Systems B)
+Sys₁ {A} {B} f = record
+    { F₀ = map f
+    ; F₁ = λ C≤D → map-≤ f C≤D
+    ; identity = map-≤-refl f
+    ; homomorphism = map-≤-trans f
+    ; F-resp-≈ = map-≈ f
+    }
+
+opaque
+  unfolding map
+  map-id-≤ : (X : System A) → map id X ≤ X
+  map-id-≤ X .⇒S = Id (S X)
+  map-id-≤ X .≗-fₛ i s = cong (fₛ X) Pull.identity
+  map-id-≤ X .≗-fₒ s = Push.identity
+
+opaque
+  unfolding map
+  map-id-≥ : (X : System A) → X ≤ map id X
+  map-id-≥ X .⇒S = Id (S X)
+  map-id-≥ X .≗-fₛ i s = cong (fₛ X) (≋.sym Pull.identity)
+  map-id-≥ X .≗-fₒ s = ≋.sym Push.identity
+
+opaque
+  unfolding map-≤ map-id-≤
+  map-id-comm
+      : {X Y : System A}
+        (f : X ≤ Y)
+      → ≤-trans (map-≤ id f) (map-id-≤ Y) ≈ ≤-trans (map-id-≤ X) f
+  map-id-comm {Y} f = Setoid.refl (S Y)
+
+opaque
+
+  unfolding map-id-≤ map-id-≥
+
+  map-id-isoˡ
+      : (X : System A)
+      → ≤-trans (map-id-≤ X) (map-id-≥ X) ≈ ≤-refl
+  map-id-isoˡ X = Setoid.refl (S X)
+
+  map-id-isoʳ
+      : (X : System A)
+      → ≤-trans (map-id-≥ X) (map-id-≤ X) ≈ ≤-refl
+  map-id-isoʳ X = Setoid.refl (S X)
+
+Sys-identity : Sys₁ {A} id ≃ idF
+Sys-identity = niHelper record
+    { η = map-id-≤
+    ; η⁻¹ = map-id-≥
+    ; commute = map-id-comm
+    ; iso = λ X → record
+        { isoˡ = map-id-isoˡ X
+        ; isoʳ = map-id-isoʳ X
+        }
+    }
+
+opaque
+  unfolding map
+  map-∘-≤
+      : (f : Fin A → Fin B)
+        (g : Fin B → Fin C)
+        (X : System A)
+      → map (g ∘ f) X ≤ map g (map f X)
+  map-∘-≤ f g X .⇒S = Id (S X)
+  map-∘-≤ f g X .≗-fₛ i s = cong (fₛ X) Pull.homomorphism
+  map-∘-≤ f g X .≗-fₒ s = Push.homomorphism
+
+opaque
+  unfolding map
+  map-∘-≥
+      : (f : Fin A → Fin B)
+        (g : Fin B → Fin C)
+        (X : System A)
+      → map g (map f X) ≤ map (g ∘ f) X
+  map-∘-≥ f g X .⇒S = Id (S X)
+  map-∘-≥ f g X .≗-fₛ i s = cong (fₛ X) (≋.sym Pull.homomorphism)
+  map-∘-≥ f g X .≗-fₒ s = ≋.sym Push.homomorphism
+
+Sys-homo
+    : (f : Fin A → Fin B)
+      (g : Fin B → Fin C)
+    → Sys₁ (g ∘ f) ≃ Sys₁ g ∘F Sys₁ f
+Sys-homo {A} f g = niHelper record
+    { η = map-∘-≤ f g
+    ; η⁻¹ = map-∘-≥ f g
+    ; commute = map-∘-comm f g
+    ; iso = λ X → record
+        { isoˡ = isoˡ X
+        ; isoʳ = isoʳ X
         }
+    }
+  where
+    opaque
+      unfolding map-∘-≤ map-≤
+      map-∘-comm
+          : (f : Fin A → Fin B)
+            (g : Fin B → Fin C)
+          → {X Y : System A}
+            (X≤Y : X ≤ Y)
+          → ≤-trans (map-≤ (g ∘ f) X≤Y) (map-∘-≤ f g Y)
+          ≈ ≤-trans (map-∘-≤ f g X) (map-≤ g (map-≤ f X≤Y))
+      map-∘-comm f g {Y} X≤Y = Setoid.refl (S Y)
+    module _ (X : System A) where
+      opaque
+        unfolding map-∘-≤ map-∘-≥
+        isoˡ : ≤-trans (map-∘-≤ f g X) (map-∘-≥ f g X) ≈ ≤-refl
+        isoˡ = Setoid.refl (S X)
+        isoʳ : ≤-trans (map-∘-≥ f g X) (map-∘-≤ f g X) ≈ ≤-refl
+        isoʳ = Setoid.refl (S X)
 
-    ≤-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
+module _ {f g : Fin A → Fin B} (f≗g : f ≗ g) (X : System A) where
 
   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
+    unfolding map
+
+    map-cong-≤ : map f X ≤ map g X
+    map-cong-≤ .⇒S = Id (S X)
+    map-cong-≤ .≗-fₛ i s = cong (fₛ X) (Pull.F-resp-≈ f≗g)
+    map-cong-≤ .≗-fₒ s = Push.F-resp-≈ f≗g
+
+    map-cong-≥ : map g X ≤ map f X
+    map-cong-≥ .⇒S = Id (S X)
+    map-cong-≥ .≗-fₛ i s = cong (fₛ X) (Pull.F-resp-≈ (≡.sym ∘ f≗g))
+    map-cong-≥ .≗-fₒ s = Push.F-resp-≈ (≡.sym ∘ f≗g)
 
 opaque
-  unfolding System₁
-  Sys-defs : ⊤
-  Sys-defs = tt
-
-Sys : Functor Nat (Setoids (suc 0ℓ) (suc 0ℓ))
-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-≈
+  unfolding map-≤ map-cong-≤
+  map-cong-comm
+      : {f g : Fin A → Fin B}
+        (f≗g : f ≗ g)
+        {X Y : System A}
+        (h : X ≤ Y)
+      → ≤-trans (map-≤ f h) (map-cong-≤ f≗g Y)
+      ≈ ≤-trans (map-cong-≤ f≗g X) (map-≤ g h)
+  map-cong-comm f≗g {Y} h = Setoid.refl (S Y)
+
+opaque
+
+  unfolding map-cong-≤
+
+  map-cong-isoˡ
+      : {f g : Fin A → Fin B}
+        (f≗g : f ≗ g)
+        (X : System A)
+      → ≤-trans (map-cong-≤ f≗g X) (map-cong-≥ f≗g X) ≈ ≤-refl
+  map-cong-isoˡ f≗g X = Setoid.refl (S X)
+
+  map-cong-isoʳ
+      : {f g : Fin A → Fin B}
+        (f≗g : f ≗ g)
+        (X : System A)
+      → ≤-trans (map-cong-≥ f≗g X) (map-cong-≤ f≗g X) ≈ ≤-refl
+  map-cong-isoʳ f≗g X = Setoid.refl (S X)
+
+Sys-resp-≈ : {f g : Fin A → Fin B} → f ≗ g → Sys₁ f ≃ Sys₁ g
+Sys-resp-≈ f≗g = niHelper record
+    { η = map-cong-≤ f≗g
+    ; η⁻¹ = map-cong-≥ f≗g
+    ; commute = map-cong-comm f≗g
+    ; iso = λ X → record
+        { isoˡ = map-cong-isoˡ f≗g X
+        ; isoʳ = map-cong-isoʳ f≗g X
+        }
+    }
+
+Sys : Functor Nat (Cats (suc 0ℓ) (suc 0ℓ) 0ℓ)
+Sys .F₀ = Systems
+Sys .F₁ = Sys₁
+Sys .identity = Sys-identity
+Sys .homomorphism = Sys-homo _ _
+Sys .F-resp-≈ = Sys-resp-≈
 
 module Sys = Functor Sys