Clean up System functors

author: Jacques Comeaux <jacquesrcomeaux@protonmail.com> 2025-11-09 17:12:29 -0600
committer: Jacques Comeaux <jacquesrcomeaux@protonmail.com> 2025-11-09 17:12:29 -0600
commit: 6a5154cf29d98ab644b5def52c55f213d1076e2b (patch)
tree: 2a6ddd6034607f36f4441fe3d1bd6e71e4264cb3
parent: b2b2bdaa75406451174f0873cfd355e7511abd9a (diff)
11 files changed, 1120 insertions, 980 deletions
diff --git a/Data/Circuit/Merge.agda b/Data/Circuit/Merge.agda
index 82c0d92..9cf180a 100644
--- a/Data/Circuit/Merge.agda
+++ b/Data/Circuit/Merge.agda
@@ -3,11 +3,12 @@
 module Data.Circuit.Merge where
 
 open import Data.Nat.Base using (ℕ)
-open import Data.Fin.Base using (Fin; pinch; punchIn; punchOut)
+open import Data.Fin.Base using (Fin; pinch; punchIn; punchOut; splitAt)
 open import Data.Fin.Properties using (punchInᵢ≢i; punchIn-punchOut)
 open import Data.Bool.Properties using (if-eta)
 open import Data.Bool using (Bool; if_then_else_)
 open import Data.Circuit.Value using (Value; join; join-comm; join-assoc)
+open import Data.Sum.Properties using ([,]-cong; [,-]-cong; [-,]-cong; [,]-∘; [,]-map)
 open import Data.Subset.Functional
   using
       ( Subset
@@ -18,6 +19,7 @@ open import Data.Subset.Functional
       ; foldl-fusion
       )
 open import Data.Vector as V using (Vector; head; tail; removeAt)
+open import Data.Vec.Functional using (_++_)
 open import Data.Fin.Permutation
   using
     ( Permutation
@@ -31,14 +33,16 @@ open import Data.Fin.Permutation
     )
 open import Data.Product using (Σ-syntax; _,_)
 open import Data.Fin.Preimage using (preimage; preimage-cong₁; preimage-cong₂)
-open import Function.Base using (∣_⟩-_; _∘_)
-open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_)
+open import Function.Base using (∣_⟩-_; _∘_; case_of_; _$_)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≢_; _≗_; module ≡-Reasoning)
 
 open Value using (U)
 open ℕ
 open Fin
 open Bool
 
+open ≡-Reasoning
+
 _when_ : Value → Bool → Value
 x when b = if b then x else U
 
@@ -90,8 +94,6 @@ merge-with-U {suc A} e S = begin
     merge-with e (tail (λ _ → U)) (tail S)  ≡⟨⟩
     merge-with e (λ _ → U) (tail S)         ≡⟨ merge-with-U e (tail S) ⟩
     e                                       ∎
-  where
-    open ≡.≡-Reasoning
 
 merge : {A : ℕ} → Vector Value A → Subset A → Value
 merge v = merge-with U v
@@ -146,8 +148,6 @@ merge-removeAt {A} zero v S = begin
     merge-with U v S                                            ≡⟨ merge-suc v S ⟩
     merge-with (head v when head S) (tail v) (tail S)           ≡⟨ join-merge (head v when head S) (tail v) (tail S) ⟨
     join (head v when head S) (merge-with U (tail v) (tail S))  ∎
-  where
-    open ≡.≡-Reasoning
 merge-removeAt {suc A} (suc k) v S = begin
     merge-with U v S                                  ≡⟨ merge-suc v S ⟩
     merge-with v0? (tail v) (tail S)                  ≡⟨ join-merge _ (tail v) (tail S) ⟨
@@ -166,7 +166,6 @@ merge-removeAt {suc A} (suc k) v S = begin
     v- = removeAt v (suc k)
     S- : Subset (suc A)
     S- = removeAt S (suc k)
-    open ≡.≡-Reasoning
 
 import Function.Structures as FunctionStructures
 open module FStruct {A B : Set} = FunctionStructures {_} {_} {_} {_} {A} _≡_ {B} _≡_ using (IsInverse)
@@ -211,7 +210,6 @@ merge-preimage-ρ {suc A} {suc B} ρ v S = begin
     S- = tail S
     vρˡ0? : Value
     vρˡ0? = head (v ∘ ρˡ) when head S
-    open ≡.≡-Reasoning
     ≡vρˡ0?  : head (v ∘ ρˡ) when S (ρʳ (head ρˡ)) ≡ head (v ∘ ρˡ) when head S
     ≡vρˡ0? = ≡.cong ((head (v ∘ ρˡ) when_) ∘ S) (inverseʳ ρ)
     v∘ρˡ- : v- ∘ ρˡ- ≗ tail (v ∘ ρˡ)
@@ -252,8 +250,6 @@ mutual
       U                       ≡⟨ merge-with-U U S ⟨
       merge (λ _ → U) S       ≡⟨ merge-cong₁ (λ x → ≡.sym (merge-[] v (⁅ x ⁆ ∘ f))) S ⟩
       merge (push v f) S      ∎
-    where
-      open ≡.≡-Reasoning
   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
@@ -266,7 +262,6 @@ mutual
           merge (merge v ∘ preimage (ρˡ ∘ ρʳ ∘ f) ∘ ⁅_⁆) S          ≡⟨ merge-cong₁ (merge-cong₂ v ∘ preimage-cong₁ (λ y → inverseˡ ρ {f y}) ∘ ⁅_⁆) S ⟩
           merge (merge v ∘ preimage f ∘ ⁅_⁆) S                      ∎
         where
-          open ≡.≡-Reasoning
           ρʳ ρˡ : Fin (ℕ.suc B) → Fin (ℕ.suc B)
           ρʳ = ρ ⟨$⟩ʳ_
           ρˡ = ρ ⟨$⟩ˡ_
@@ -319,7 +314,6 @@ mutual
             v0? = v0 when f⁻¹[S]0
             v0?+[f[v-]0?] = (if S0 then join v0? f[v-]0 else v0?)
             f[v]0? = f[v]0 when S0
-            open ≡.≡-Reasoning
             ≡f[v]0 : v0?+[f[v-]0?] ≡ f[v]0?
             ≡f[v]0 rewrite f0≡0 with S0
             ... | true = begin
@@ -339,3 +333,95 @@ mutual
               where
                 v0?′ : Value
                 v0?′ = v0 when head (preimage f ⁅ suc x ⁆)
+
+merge-++
+    : {n m : ℕ}
+      (xs : Vector Value n)
+      (ys : Vector Value m)
+      (S₁ : Subset n)
+      (S₂ : Subset m)
+    → merge (xs ++ ys) (S₁ ++ S₂)
+    ≡ join (merge xs S₁) (merge ys S₂)
+merge-++ {zero} {m} xs ys S₁ S₂ = begin
+    merge (xs ++ ys) (S₁ ++ S₂)       ≡⟨ merge-cong₂ (xs ++ ys) (λ _ → ≡.refl) ⟩
+    merge (xs ++ ys) S₂               ≡⟨ merge-cong₁ (λ _ → ≡.refl) S₂ ⟩
+    merge ys S₂                       ≡⟨ ≡.cong (λ h → join h (merge ys S₂)) (merge-[] xs S₁) ⟨
+    join (merge xs S₁) (merge ys S₂)  ∎
+merge-++ {suc n} {m} xs ys S₁ S₂ = begin
+    merge (xs ++ ys) (S₁ ++ S₂)                                                   ≡⟨ merge-suc (xs ++ ys) (S₁ ++ S₂) ⟩
+    merge-with (head xs when head S₁) (tail (xs ++ ys)) (tail (S₁ ++ S₂))         ≡⟨ join-merge (head xs when head S₁) (tail (xs ++ ys)) (tail (S₁ ++ S₂)) ⟨
+    join (head xs when head S₁) (merge (tail (xs ++ ys)) (tail (S₁ ++ S₂)))
+        ≡⟨ ≡.cong (join (head xs when head S₁)) (merge-cong₁ ([,]-map ∘ splitAt n) (tail (S₁ ++ S₂))) ⟩
+    join (head xs when head S₁) (merge (tail xs ++ ys) (tail (S₁ ++ S₂)))
+        ≡⟨ ≡.cong (join (head xs when head S₁)) (merge-cong₂ (tail xs ++ ys) ([,]-map ∘ splitAt n)) ⟩
+    join (head xs when head S₁) (merge (tail xs ++ ys) (tail S₁ ++ S₂))           ≡⟨ ≡.cong (join (head xs when head S₁)) (merge-++ (tail xs) ys (tail S₁) S₂) ⟩
+    join (head xs when head S₁) (join (merge (tail xs) (tail S₁)) (merge ys S₂))  ≡⟨ join-assoc (head xs when head S₁) (merge (tail xs) (tail S₁)) _ ⟨
+    join (join (head xs when head S₁) (merge (tail xs) (tail S₁))) (merge ys S₂)
+        ≡⟨ ≡.cong (λ h → join h (merge ys S₂)) (join-merge (head xs when head S₁) (tail xs) (tail S₁)) ⟩
+    join (merge-with (head xs when head S₁) (tail xs) (tail S₁)) (merge ys S₂)    ≡⟨ ≡.cong (λ h → join h (merge ys S₂)) (merge-suc xs S₁) ⟨
+    join (merge xs S₁) (merge ys S₂)                                              ∎
+
+open import Function using (Equivalence)
+open Equivalence
+open import Data.Nat using (_+_)
+open import Data.Fin using (_↑ˡ_; _↑ʳ_; _≟_)
+open import Data.Fin.Properties using (↑ˡ-injective; ↑ʳ-injective; splitAt⁻¹-↑ˡ; splitAt-↑ˡ; splitAt⁻¹-↑ʳ; splitAt-↑ʳ)
+open import Relation.Nullary.Decidable using (does; does-⇔; dec-false)
+
+open Fin
+⁅⁆-≟ : {n : ℕ} (x y : Fin n) → ⁅ x ⁆ y ≡ does (x ≟ y)
+⁅⁆-≟ zero zero = ≡.refl
+⁅⁆-≟ zero (suc y) = ≡.refl
+⁅⁆-≟ (suc x) zero = ≡.refl
+⁅⁆-≟ (suc x) (suc y) = ⁅⁆-≟ x y
+
+open import Data.Sum using ([_,_]′; inj₁; inj₂)
+⁅⁆-++
+    : {n′ m′ : ℕ}
+      (i : Fin (n′ + m′))
+    → [ (λ x → ⁅ x ⁆ ++ ⊥) , (λ x → ⊥ ++ ⁅ x ⁆) ]′ (splitAt n′ i) ≗ ⁅ i ⁆
+⁅⁆-++ {n′} {m′} i x with splitAt n′ i in eq₁
+... | inj₁ i′ with splitAt n′ x in eq₂
+...   | inj₁ x′ = begin
+            ⁅ i′ ⁆ x′                   ≡⟨ ⁅⁆-≟ i′ x′ ⟩
+            does (i′ ≟ x′)              ≡⟨ does-⇔ ⇔ (i′ ≟ x′) (i′ ↑ˡ m′ ≟ x′ ↑ˡ m′) ⟩
+            does (i′ ↑ˡ m′ ≟ x′ ↑ˡ m′)  ≡⟨ ⁅⁆-≟ (i′ ↑ˡ m′) (x′ ↑ˡ m′) ⟨
+            ⁅ i′ ↑ˡ m′ ⁆ (x′ ↑ˡ m′)     ≡⟨ ≡.cong₂ ⁅_⁆ (splitAt⁻¹-↑ˡ eq₁) (splitAt⁻¹-↑ˡ eq₂) ⟩
+            ⁅ i ⁆ x                 ∎
+          where
+            ⇔ : Equivalence (≡.setoid (i′ ≡ x′)) (≡.setoid (i′ ↑ˡ m′ ≡ x′ ↑ˡ m′))
+            ⇔ .to = ≡.cong (_↑ˡ m′)
+            ⇔ .from = ↑ˡ-injective m′ i′ x′
+            ⇔ .to-cong ≡.refl = ≡.refl
+            ⇔ .from-cong ≡.refl = ≡.refl
+...   | inj₂ x′ = begin
+            false                       ≡⟨ dec-false (i′ ↑ˡ m′ ≟ n′ ↑ʳ x′) ↑ˡ≢↑ʳ ⟨
+            does (i′ ↑ˡ m′ ≟ n′ ↑ʳ x′)  ≡⟨ ⁅⁆-≟ (i′ ↑ˡ m′) (n′ ↑ʳ x′) ⟨
+            ⁅ i′ ↑ˡ m′ ⁆ (n′ ↑ʳ x′)     ≡⟨ ≡.cong₂ ⁅_⁆ (splitAt⁻¹-↑ˡ eq₁) (splitAt⁻¹-↑ʳ eq₂) ⟩
+            ⁅ i ⁆ x                     ∎
+          where
+            ↑ˡ≢↑ʳ : i′ ↑ˡ m′ ≢ n′ ↑ʳ x′
+            ↑ˡ≢↑ʳ ≡ = case ≡.trans (≡.sym (splitAt-↑ˡ n′ i′ m′)) (≡.trans (≡.cong (splitAt n′) ≡) (splitAt-↑ʳ n′ m′ x′)) of λ { () }
+⁅⁆-++ {n′} i x | inj₂ i′ with splitAt n′ x in eq₂
+⁅⁆-++ {n′} {m′} i x | inj₂ i′ | inj₁ x′ = begin
+    [ ⊥ , ⁅ i′ ⁆ ]′ (splitAt n′ x)  ≡⟨ ≡.cong ([ ⊥ , ⁅ i′ ⁆ ]′) eq₂ ⟩
+    false                           ≡⟨ dec-false (n′ ↑ʳ i′ ≟ x′ ↑ˡ m′) ↑ʳ≢↑ˡ ⟨
+    does (n′ ↑ʳ i′ ≟ x′ ↑ˡ m′)      ≡⟨ ⁅⁆-≟ (n′ ↑ʳ i′) (x′ ↑ˡ m′) ⟨
+    ⁅ n′ ↑ʳ i′ ⁆ (x′ ↑ˡ m′)         ≡⟨ ≡.cong₂ ⁅_⁆ (splitAt⁻¹-↑ʳ eq₁) (splitAt⁻¹-↑ˡ eq₂) ⟩
+    ⁅ i ⁆ x                         ∎
+  where
+    ↑ʳ≢↑ˡ : n′ ↑ʳ i′ ≢ x′ ↑ˡ m′
+    ↑ʳ≢↑ˡ ≡ = case ≡.trans (≡.sym (splitAt-↑ʳ n′ m′ i′)) (≡.trans (≡.cong (splitAt n′) ≡) (splitAt-↑ˡ n′ x′ m′)) of λ { () }
+⁅⁆-++ {n′} i x | inj₂ i′ | inj₂ x′ = begin
+    [ ⊥ , ⁅ i′ ⁆ ]′ (splitAt n′ x)  ≡⟨ ≡.cong [ ⊥ , ⁅ i′ ⁆ ]′ eq₂ ⟩
+    ⁅ i′ ⁆ x′                       ≡⟨ ⁅⁆-≟ i′ x′ ⟩
+    does (i′ ≟ x′)                  ≡⟨ does-⇔ ⇔ (i′ ≟ x′) (n′ ↑ʳ i′ ≟ n′ ↑ʳ x′) ⟩
+    does (n′ ↑ʳ i′ ≟ n′ ↑ʳ x′)      ≡⟨ ⁅⁆-≟ (n′ ↑ʳ i′) (n′ ↑ʳ x′) ⟨
+    ⁅ n′ ↑ʳ i′ ⁆ (n′ ↑ʳ x′)         ≡⟨ ≡.cong₂ ⁅_⁆ (splitAt⁻¹-↑ʳ eq₁) (splitAt⁻¹-↑ʳ eq₂) ⟩
+    ⁅ i ⁆ x                         ∎
+  where
+    ⇔ : Equivalence (≡.setoid (i′ ≡ x′)) (≡.setoid (n′ ↑ʳ i′ ≡ n′ ↑ʳ x′))
+    ⇔ .to = ≡.cong (n′ ↑ʳ_)
+    ⇔ .from = ↑ʳ-injective n′ i′ x′
+    ⇔ .to-cong ≡.refl = ≡.refl
+    ⇔ .from-cong ≡.refl = ≡.refl
diff --git a/Data/Circuit/Value.agda b/Data/Circuit/Value.agda
index 512a622..b135c35 100644
--- a/Data/Circuit/Value.agda
+++ b/Data/Circuit/Value.agda
@@ -2,12 +2,22 @@
 
 module Data.Circuit.Value where
 
-open import Relation.Binary.Lattice.Bundles using (BoundedJoinSemilattice)
+import Relation.Binary.Lattice.Properties.BoundedJoinSemilattice as LatticeProp
+
+open import Algebra.Bundles using (CommutativeMonoid)
+open import Algebra.Structures using (IsCommutativeMonoid; IsMonoid; IsSemigroup; IsMagma)
 open import Data.Product.Base using (_×_; _,_)
 open import Data.String.Base using (String)
 open import Level using (0ℓ)
+open import Relation.Binary.Lattice.Bundles using (BoundedJoinSemilattice)
 open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
 
+open CommutativeMonoid
+open IsCommutativeMonoid
+open IsMagma
+open IsMonoid
+open IsSemigroup
+
 data Value : Set where
   U T F X : Value
 
@@ -129,8 +139,8 @@ join-assoc X X T = ≡.refl
 join-assoc X X F = ≡.refl
 join-assoc X X X = ≡.refl
 
-ValueLattice : BoundedJoinSemilattice 0ℓ 0ℓ 0ℓ
-ValueLattice = record
+Lattice : BoundedJoinSemilattice 0ℓ 0ℓ 0ℓ
+Lattice = record
     { Carrier = Value
     ; _≈_ = _≡_
     ; _≤_ = ≤-Value
@@ -155,3 +165,16 @@ ValueLattice = record
             X → U≤X
         }
     }
+
+module Lattice = BoundedJoinSemilattice Lattice
+
+Monoid : CommutativeMonoid 0ℓ 0ℓ
+Monoid .Carrier = Lattice.Carrier
+Monoid ._≈_ = Lattice._≈_
+Monoid ._∙_ = Lattice._∨_
+Monoid .ε = Lattice.⊥
+Monoid .isCommutativeMonoid .isMonoid .isSemigroup .isMagma .isEquivalence = ≡.isEquivalence
+Monoid .isCommutativeMonoid .isMonoid .isSemigroup .isMagma .∙-cong = ≡.cong₂ join
+Monoid .isCommutativeMonoid .isMonoid .isSemigroup .assoc = join-assoc
+Monoid .isCommutativeMonoid .isMonoid .identity = LatticeProp.identity Lattice
+Monoid .isCommutativeMonoid .comm = join-comm
diff --git a/Data/System.agda b/Data/System.agda
index cecdfcd..5d5e484 100644
--- a/Data/System.agda
+++ b/Data/System.agda
@@ -1,85 +1,144 @@
 {-# OPTIONS --without-K --safe #-}
 
 open import Level using (Level; 0ℓ; suc)
+
 module Data.System {ℓ : Level} where
 
-import Function.Construct.Identity as Id
 import Relation.Binary.Properties.Preorder as PreorderProperties
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 
-open import Data.Circuit.Value using (Value)
-open import Data.Nat.Base using (ℕ)
+open import Categories.Category using (Category)
+open import Categories.Category.Instance.SingletonSet using () renaming (SingletonSetoid to ⊤ₛ)
+open import Data.Circuit.Value using (Monoid)
+open import Data.Nat using (ℕ)
 open import Data.Setoid using (_⇒ₛ_; ∣_∣)
-open import Data.System.Values Value using (Values; _≋_; module ≋)
+open import Data.System.Values Monoid using (Values; _≋_; module ≋; <ε>)
+open import Function using (Func; _⟨$⟩_; flip)
+open import Function.Construct.Constant using () renaming (function to Const)
+open import Function.Construct.Identity using () renaming (function to Id)
+open import Function.Construct.Setoid using (_∙_)
 open import Level using (Level; 0ℓ; suc)
+open import Relation.Binary as Rel using (Reflexive; Transitive; Preorder; Setoid; Rel)
 open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
-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 Func
 
-record System (n : ℕ) : Set₁ where
-
-  field
-    S : Setoid 0ℓ 0ℓ
-    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
 
-module _ {n : ℕ} where
+  record System : Set₁ 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)
+      S : Setoid 0ℓ 0ℓ
+      fₛ : ∣ Values n ⇒ₛ S ⇒ₛ S ∣
+      fₒ : ∣ S ⇒ₛ Values n ∣
 
-  open ≤-System
+    fₛ′ : ∣ Values n ∣ → ∣ S ∣ → ∣ S ∣
+    fₛ′ i = to (to fₛ i)
 
-  ≤-refl : Reflexive ≤-System
-  ⇒S ≤-refl = Id.function _
-  ≗-fₛ (≤-refl {x}) _ _ = System.refl x
-  ≗-fₒ (≤-refl {x}) _ = ≋.refl
+    fₒ′ : ∣ S ∣ → ∣ Values n ∣
+    fₒ′ = to fₒ
 
-  ≡⇒≤ : _≡_ ⇒ ≤-System
-  ≡⇒≤ ≡.refl = ≤-refl
+    module S = Setoid S
 
   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 0ℓ) (suc 0ℓ) ℓ
-  System-Preorder = record
-      { Carrier = System n
-      ; _≈_ = _≡_
-      ; _≲_ = ≤-System
-      ; isPreorder = record
-          { isEquivalence = ≡.isEquivalence
-          ; reflexive = ≡⇒≤
-          ; trans = ≤-trans
-          }
-      }
+  discrete : System
+  discrete .S = ⊤ₛ
+  discrete .fₛ = Const (Values n) (⊤ₛ ⇒ₛ ⊤ₛ) (Id ⊤ₛ)
+  discrete .fₒ = Const ⊤ₛ (Values n) <ε>
 
-module _ (n : ℕ) where
+module _ {n : ℕ} where
 
-  open PreorderProperties (System-Preorder {n}) using (InducedEquivalence)
+  record _≤_ (a b : System n) : Set ℓ where
 
-  Systemₛ : Setoid (suc 0ℓ) ℓ
-  Systemₛ = InducedEquivalence
+    private
+      module A = System a
+      module B = System b
+
+    open B using (S)
+
+    field
+      ⇒S : ∣ A.S ⇒ₛ B.S ∣
+      ≗-fₛ : (i : ∣ Values n ∣) (s : ∣ A.S ∣) → ⇒S ⟨$⟩ (A.fₛ′ i s) S.≈ B.fₛ′ i (⇒S ⟨$⟩ s)
+      ≗-fₒ : (s : ∣ A.S ∣) → A.fₒ′ s ≋ B.fₒ′ (⇒S ⟨$⟩ s)
+
+  infix 4 _≤_
+
+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)
+
+System-≤ : ℕ → Preorder (suc 0ℓ) (suc 0ℓ) ℓ
+System-≤ n = record
+    { _≲_ = _≤_ {n}
+    ; isPreorder = record
+        { isEquivalence = ≡.isEquivalence
+        ; reflexive = ≡⇒≤
+        ; trans = ≤-trans
+        }
+    }
+
+Systemₛ : ℕ → Setoid (suc 0ℓ) ℓ
+Systemₛ n = PreorderProperties.InducedEquivalence (System-≤ n)
+
+Systems : ℕ → Category (suc 0ℓ) ℓ 0ℓ
+Systems n = record
+    { Obj = System n
+    ; _⇒_ = _≤_
+    ; _≈_ = _≈_
+    ; id = ≤-refl
+    ; _∘_ = flip ≤-trans
+    ; assoc = λ {D = D} → S.refl D
+    ; sym-assoc = λ {D = D} → S.refl D
+    ; identityˡ = λ {B = B} → S.refl B
+    ; identityʳ = λ {B = B} → S.refl B
+    ; identity² = λ {A = A} → S.refl A
+    ; equiv = ≈-isEquiv
+    ; ∘-resp-≈ = λ {f = f} {h} {g} {i} → ≤-resp-≈ {f = f} {h} {g} {i}
+    }
diff --git a/Data/System/Values.agda b/Data/System/Values.agda
index bf8fa38..737e34e 100644
--- a/Data/System/Values.agda
+++ b/Data/System/Values.agda
@@ -1,21 +1,95 @@
 {-# OPTIONS --without-K --safe #-}
 
-module Data.System.Values (A : Set) where
+open import Algebra.Bundles using (CommutativeMonoid)
+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.Properties as VecProps
+import Relation.Binary.PropositionalEquality as ≡
 
-open import Data.Nat.Base using (ℕ)
-open import Data.Vec.Functional using (Vector)
+open import Data.Fin using (_↑ˡ_; _↑ʳ_; zero; suc)
+open import Data.Nat using (ℕ; _+_; suc)
+open import Data.Product using (_,_)
+open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
+open import Data.Setoid using (∣_∣)
+open import Data.Vec.Functional as Vec using (Vector; zipWith; replicate)
+open import Data.Vec.Functional.Relation.Binary.Equality.Setoid using (≋-setoid)
+open import Function using (Func; _⟶ₛ_; _⟨$⟩_; _∘_)
 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 ≡
+open CommutativeMonoid A renaming (Carrier to Value)
+open Func
+open Sum A using (sum)
+
+opaque
+
+  Values : ℕ → Setoid 0ℓ 0ℓ
+  Values = ≋-setoid (≡.setoid Value)
+
+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 ε
+
+    head : ∣ Values (suc n) ∣ → Value
+    head xs = xs zero
+
+    tail : ∣ Values (suc n) ∣ → ∣ Values n ∣
+    tail xs = xs ∘ suc
+
+  module ≋ = Setoid (Values n)
+
+  _≋_ : Rel ∣ Values n ∣ 0ℓ
+  _≋_ = ≋._≈_
+
+  infix 4 _≋_
+
+opaque
+
+  unfolding Values
+
+  [] : ∣ Values 0 ∣
+  [] = Vec.[]
+
+  []-unique : (xs ys : ∣ Values 0 ∣) → xs ≋ ys
+  []-unique xs ys ()
+
+module _ {n m : ℕ} where
+
+  opaque
+
+    unfolding Values
+
+    _++_ : ∣ Values n ∣ → ∣ Values m ∣ → ∣ Values (n + m) ∣
+    _++_ = Vec._++_
 
-Values : ℕ → Setoid 0ℓ 0ℓ
-Values = ≋-setoid (≡.setoid A)
+    infixr 5 _++_
 
-_≋_ : {n : ℕ} → Rel (Vector A n) 0ℓ
-_≋_ {n} = Setoid._≈_ (Values n)
+    ++-cong
+        : (xs xs′ : ∣ Values n ∣)
+          {ys ys′ : ∣ Values m ∣}
+        → xs ≋ xs′
+        → ys ≋ ys′
+        → xs ++ ys ≋ xs′ ++ ys′
+    ++-cong xs xs′ = VecProps.++-cong xs xs′
 
-infix 4 _≋_
+    splitₛ : Values (n + m) ⟶ₛ Values n ×ₛ Values m
+    to splitₛ v = v ∘ (_↑ˡ m) , v ∘ (n ↑ʳ_)
+    cong splitₛ v₁≋v₂ = v₁≋v₂ ∘ (_↑ˡ m) , v₁≋v₂ ∘ (n ↑ʳ_)
 
-module ≋ {n : ℕ} = Setoid (Values n)
+  ++ₛ : Values n ×ₛ Values m ⟶ₛ Values (n + m)
+  to ++ₛ (xs , ys) = xs ++ ys
+  cong ++ₛ (≗xs , ≗ys) = ++-cong _ _ ≗xs ≗ys
diff --git a/Data/Vector.agda b/Data/Vector.agda
index 052f624..874f0b2 100644
--- a/Data/Vector.agda
+++ b/Data/Vector.agda
@@ -3,10 +3,10 @@
 module Data.Vector where
 
 open import Data.Nat.Base using (ℕ)
-open import Data.Vec.Functional using (Vector; head; tail; []; removeAt; map) public
-open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_)
+open import Data.Vec.Functional using (Vector; head; tail; []; removeAt; map; _++_) public
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_; module ≡-Reasoning)
 open import Function.Base using (∣_⟩-_; _∘_)
-open import Data.Fin.Base using (Fin; toℕ)
+open import Data.Fin.Base using (Fin; toℕ; _↑ˡ_; _↑ʳ_)
 open ℕ
 open Fin
 
@@ -80,3 +80,47 @@ foldl-[]
       {e : B 0}
     → foldl B f e [] ≡ e
 foldl-[] _ _ = ≡.refl
+
+open import Data.Sum using ([_,_]′)
+open import Data.Sum.Properties using ([,-]-cong; [-,]-cong; [,]-∘)
+open import Data.Fin.Properties using (splitAt-↑ˡ; splitAt-↑ʳ)
+open import Data.Fin using (splitAt)
+open import Data.Nat using (_+_)
+++-↑ˡ
+    : {n m : ℕ}
+      {A : Set}
+      (X : Vector A n)
+      (Y : Vector A m)
+    → (X ++ Y) ∘ (_↑ˡ m) ≗ X
+++-↑ˡ {n} {m} X Y i = ≡.cong [ X , Y ]′ (splitAt-↑ˡ n i m)
+
+++-↑ʳ
+    : {n m : ℕ}
+      {A : Set}
+      (X : Vector A n)
+      (Y : Vector A m)
+    → (X ++ Y) ∘ (n ↑ʳ_) ≗ Y
+++-↑ʳ {n} {m} X Y i = ≡.cong [ X , Y ]′ (splitAt-↑ʳ n m i)
+
++-assocʳ : {m n o : ℕ} → Fin (m + (n + o)) → Fin (m + n + o)
++-assocʳ {m} {n} {o} = [ (λ x → x ↑ˡ n ↑ˡ o) , [ (λ x → (m ↑ʳ x) ↑ˡ o) , m + n ↑ʳ_  ]′ ∘ splitAt n ]′ ∘ splitAt m
+
+open ≡-Reasoning
+++-assoc
+    : {m n o : ℕ}
+      {A : Set}
+      (X : Vector A m)
+      (Y : Vector A n)
+      (Z : Vector A o)
+    → ((X ++ Y) ++ Z) ∘ +-assocʳ {m} ≗ X ++ (Y ++ Z)
+++-assoc {m} {n} {o} X Y Z i = begin
+    ((X ++ Y) ++ Z) (+-assocʳ {m} i)                                          ≡⟨⟩
+    ((X ++ Y) ++ Z) ([ (λ x → x ↑ˡ n ↑ˡ o) , _ ]′ (splitAt m i))              ≡⟨ [,]-∘ ((X ++ Y) ++ Z) (splitAt m i) ⟩
+    [ ((X ++ Y) ++ Z) ∘ (λ x → x ↑ˡ n ↑ˡ o) , _ ]′ (splitAt m i)              ≡⟨ [-,]-cong (++-↑ˡ (X ++ Y) Z ∘ (_↑ˡ n)) (splitAt m i) ⟩
+    [ (X ++ Y) ∘ (_↑ˡ n) , _ ]′ (splitAt m i)                                 ≡⟨ [-,]-cong (++-↑ˡ X Y) (splitAt m i) ⟩
+    [ X , ((X ++ Y) ++ Z) ∘ [ _ , _ ]′ ∘ splitAt n ]′ (splitAt m i)           ≡⟨ [,-]-cong ([,]-∘ ((X ++ Y) ++ Z) ∘ splitAt n) (splitAt m i) ⟩
+    [ X , [ (_ ++ Z) ∘ (_↑ˡ o) ∘ (m ↑ʳ_) , _ ]′ ∘ splitAt n ]′ (splitAt m i)  ≡⟨ [,-]-cong ([-,]-cong (++-↑ˡ (X ++ Y) Z ∘ (m ↑ʳ_)) ∘ splitAt n) (splitAt m i) ⟩
+    [ X , [ (X ++ Y) ∘ (m ↑ʳ_) , _ ]′ ∘ splitAt n ]′ (splitAt m i)            ≡⟨ [,-]-cong ([-,]-cong (++-↑ʳ X Y) ∘ splitAt n) (splitAt m i) ⟩
+    [ X , [ Y , ((X ++ Y) ++ Z) ∘ (m + n ↑ʳ_) ]′ ∘ splitAt n ]′ (splitAt m i) ≡⟨ [,-]-cong ([,-]-cong (++-↑ʳ (X ++ Y) Z) ∘ splitAt n) (splitAt m i) ⟩
+    [ X , [ Y , Z ]′ ∘ splitAt n ]′ (splitAt m i)                             ≡⟨⟩
+    (X ++ (Y ++ Z)) i                                                         ∎
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
diff --git a/Functor/Monoidal/Instance/Nat/Pull.agda b/Functor/Monoidal/Instance/Nat/Pull.agda
index c2b6958..1d3d338 100644
--- a/Functor/Monoidal/Instance/Nat/Pull.agda
+++ b/Functor/Monoidal/Instance/Nat/Pull.agda
@@ -2,191 +2,167 @@
 
 module Functor.Monoidal.Instance.Nat.Pull where
 
+import Categories.Morphism as Morphism
+
+open import Level using (0ℓ; Level)
+
+open import Category.Instance.Setoids.SymmetricMonoidal {0ℓ} {0ℓ} using (Setoids-×)
 open import Category.Monoidal.Instance.Nat using (Natop,+,0; Natop-Cartesian)
-open import Categories.Category.Instance.Nat using (Nat-Cocartesian)
-open import Categories.Category.Instance.SingletonSet using (SingletonSetoid)
-open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper)
-open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism; niHelper)
-open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-Cartesian)
+
 open import Categories.Category.BinaryProducts using (module BinaryProducts)
 open import Categories.Category.Cartesian using (Cartesian)
 open import Categories.Category.Cocartesian using (Cocartesian; BinaryCoproducts)
+open import Categories.Category.Instance.Nat using (Nat)
+open import Categories.Category.Instance.Nat using (Nat-Cocartesian)
+open import Categories.Category.Instance.SingletonSet using () renaming (SingletonSetoid to ⊤ₛ)
+open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory)
+open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-Cartesian)
 open import Categories.Category.Product using (_⁂_)
 open import Categories.Functor using (_∘F_)
-open import Data.Subset.Functional using (Subset)
-open import Data.Nat.Base using (ℕ; _+_)
-open import Relation.Binary using (Setoid)
-open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
-open import Data.Product.Base using (_,_; _×_; Σ)
-open import Data.Vec.Functional using ([]; _++_)
-open import Data.Vec.Functional.Properties using (++-cong)
-open import Data.Vec.Functional using (Vector; [])
-open import Function.Bundles using (Func; _⟶ₛ_; _⟨$⟩_)
-open import Functor.Instance.Nat.Pull using (Pull; Pull₁)
-open import Level using (0ℓ; Level)
-
+open import Categories.Functor.Monoidal.Symmetric Natop,+,0 Setoids-× using (module Strong)
+open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper)
+open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism; niHelper)
+open import Data.Circuit.Value using (Monoid)
+open import Data.Vector using (++-assoc)
+open import Data.Fin.Base using (Fin; splitAt; join)
 open import Data.Fin.Permutation using (Permutation; _⟨$⟩ʳ_; _⟨$⟩ˡ_)
-open Cartesian (Setoids-Cartesian {0ℓ} {0ℓ}) using (products)
-open BinaryProducts products using (-×-)
-open Cocartesian Nat-Cocartesian using (module Dual; _+₁_; +-assocʳ; +-comm; +-swap; +₁∘+-swap; i₁; i₂)
-open Dual.op-binaryProducts using () renaming (-×- to -+-; assocˡ∘⟨⟩ to []∘assocʳ; swap∘⟨⟩ to []∘swap)
-
-open import Data.Fin.Base using (Fin; splitAt; join; _↑ˡ_; _↑ʳ_)
+open import Data.Fin.Preimage using (preimage)
 open import Data.Fin.Properties using (splitAt-join; splitAt-↑ˡ; splitAt-↑ʳ; join-splitAt)
+open import Data.Nat.Base using (ℕ; _+_)
+open import Data.Product.Base using (_,_; _×_; Σ; proj₁; proj₂)
+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.Base using ([_,_]′; map; map₁; map₂; inj₁; inj₂)
 open import Data.Sum.Properties using ([,]-map; [,]-cong; [-,]-cong; [,-]-cong; [,]-∘)
-open import Data.Fin.Preimage using (preimage)
-open import Function.Base using (_∘_; id)
+open import Data.System.Values Monoid using (Values; <ε>; []-unique; _++_; ++ₛ; splitₛ; _≋_; [])
+open import Data.Unit.Polymorphic using (tt)
+open import Function using (Func; _⟶ₛ_; _⟨$⟩_; _∘_)
+open import Function.Construct.Constant using () renaming (function to Const)
+open import Functor.Instance.Nat.Pull using (Pull; Pull-defs)
+open import Relation.Binary using (Setoid)
 open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_; module ≡-Reasoning)
-open import Data.Bool.Base using (Bool)
-open import Data.Setoid using (∣_∣)
-open import Data.Circuit.Value using (Value)
-open import Data.System.Values Value using (Values)
-
-open import Category.Instance.Setoids.SymmetricMonoidal {0ℓ} {0ℓ} using (Setoids-×)
-open import Categories.Functor.Monoidal.Symmetric Natop,+,0 Setoids-× using (module Strong)
-open Strong using (SymmetricMonoidalFunctor)
-open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory)
 
 module Setoids-× = SymmetricMonoidalCategory Setoids-×
-import Function.Construct.Constant as Const
 
+open Cartesian (Setoids-Cartesian {0ℓ} {0ℓ}) using (products)
+
+open BinaryProducts products using (-×-)
+open Cocartesian Nat-Cocartesian using (module Dual; _+₁_; +-assocʳ; +-comm; +-swap; +₁∘+-swap; i₁; i₂)
+open Dual.op-binaryProducts using () renaming (-×- to -+-; assocˡ∘⟨⟩ to []∘assocʳ; swap∘⟨⟩ to []∘swap)
 open Func
+open Morphism (Setoids-×.U) using (_≅_; module Iso)
+open Strong using (SymmetricMonoidalFunctor)
+open ≡-Reasoning
 
-module _ where
+private
 
-  open import Categories.Morphism (Setoids-×.U) using (_≅_; module Iso)
-  open import Data.Unit.Polymorphic using (tt)
   open _≅_
   open Iso
 
-  Pull-ε : SingletonSetoid ≅ Values 0
-  from Pull-ε = Const.function SingletonSetoid (Values 0) []
-  to Pull-ε = Const.function (Values 0) SingletonSetoid tt
+  Pull-ε : ⊤ₛ ≅ Values 0
+  from Pull-ε = Const ⊤ₛ (Values 0) []
+  to Pull-ε = Const (Values 0) ⊤ₛ tt
   isoˡ (iso Pull-ε) = tt
-  isoʳ (iso Pull-ε) ()
-
-++ₛ : {n m : ℕ} → Values n ×ₛ Values m ⟶ₛ Values (n + m)
-to ++ₛ (xs , ys) = xs ++ ys
-cong ++ₛ (≗xs , ≗ys) = ++-cong _ _ ≗xs ≗ys
-
-splitₛ : {n m : ℕ} → Values (n + m) ⟶ₛ Values n ×ₛ Values m
-to (splitₛ {n} {m}) v = v ∘ (_↑ˡ m) , v ∘ (n ↑ʳ_)
-cong (splitₛ {n} {m}) v₁≋v₂ = v₁≋v₂ ∘ (_↑ˡ m) , v₁≋v₂ ∘ (n ↑ʳ_)
-
-Pull-++
-    : {n n′ m m′ : ℕ}
-      (f : Fin n → Fin n′)
-      (g : Fin m → Fin m′)
-      {xs : ∣ Values n′ ∣}
-      {ys : ∣ Values m′ ∣}
-    → (Pull₁ f ⟨$⟩ xs) ++ (Pull₁ g ⟨$⟩ ys) ≗ Pull₁ (f +₁ g) ⟨$⟩ (xs ++ ys)
-Pull-++ {n} {n′} {m} {m′} f g {xs} {ys} e = begin
-    (xs ∘ f ++ ys ∘ g) e                                            ≡⟨ [,]-map (splitAt n e) ⟨
-    [ xs , ys ]′ (map f g (splitAt n e))                            ≡⟨ ≡.cong [ xs , ys ]′ (splitAt-join n′ m′ (map f g (splitAt n e))) ⟨
-    [ xs , ys ]′ (splitAt n′ (join n′ m′ (map f g (splitAt n e))))  ≡⟨ ≡.cong ([ xs , ys ]′ ∘ splitAt n′) ([,]-map (splitAt n e)) ⟩
-    [ xs , ys ]′ (splitAt n′ ((f +₁ g) e))                          ∎
-  where
-    open ≡-Reasoning
-
-⊗-homomorphism : NaturalIsomorphism (-×- ∘F (Pull ⁂ Pull)) (Pull ∘F -+-)
-⊗-homomorphism = niHelper record
-    { η = λ (n , m) → ++ₛ {n} {m}
-    ; η⁻¹ = λ (n , m) → splitₛ {n} {m}
-    ; commute = λ (f , g) → Pull-++ f g
-    ; iso = λ (n , m) → record
-        { isoˡ = λ { {x , y} → (λ i → ≡.cong [ x , y ] (splitAt-↑ˡ n i m)) , (λ i → ≡.cong [ x , y ] (splitAt-↑ʳ n m i)) }
-        ; isoʳ = λ { {x} i → ≡.trans (≡.sym ([,]-∘ x (splitAt n i))) (≡.cong x (join-splitAt n m i)) }
-        }
-    }
-  where
-    open import Data.Sum.Base using ([_,_])
-    open import Data.Product.Base using (proj₁; proj₂)
-
-++-↑ˡ
-    : {n m : ℕ}
-      (X : ∣ Values n ∣)
-      (Y : ∣ Values m ∣)
-    → (X ++ Y) ∘ i₁ ≗ X
-++-↑ˡ {n} {m} X Y i = ≡.cong [ X , Y ]′ (splitAt-↑ˡ n i m)
-
-++-↑ʳ
-    : {n m : ℕ}
-      (X : ∣ Values n ∣)
-      (Y : ∣ Values m ∣)
-    → (X ++ Y) ∘ i₂ ≗ Y
-++-↑ʳ {n} {m} X Y i = ≡.cong [ X , Y ]′ (splitAt-↑ʳ n m i)
-
--- TODO move to Data.Vector
-++-assoc
-    : {m n o : ℕ}
-      (X : ∣ Values m ∣)
-      (Y : ∣ Values n ∣)
-      (Z : ∣ Values o ∣)
-    → ((X ++ Y) ++ Z) ∘ +-assocʳ {m} ≗ X ++ (Y ++ Z)
-++-assoc {m} {n} {o} X Y Z i = begin
-    ((X ++ Y) ++ Z) (+-assocʳ {m} i)                                    ≡⟨⟩
-    ((X ++ Y) ++ Z) ([ i₁ ∘ i₁ , _ ]′ (splitAt m i))                    ≡⟨ [,]-∘ ((X ++ Y) ++ Z) (splitAt m i) ⟩
-    [ ((X ++ Y) ++ Z) ∘ i₁ ∘ i₁ , _ ]′ (splitAt m i)                    ≡⟨ [-,]-cong (++-↑ˡ (X ++ Y) Z ∘ i₁) (splitAt m i) ⟩
-    [ (X ++ Y) ∘ i₁ , _ ]′ (splitAt m i)                                ≡⟨ [-,]-cong (++-↑ˡ X Y) (splitAt m i) ⟩
-    [ X , ((X ++ Y) ++ Z) ∘ [ _ , _ ]′ ∘ splitAt n ]′ (splitAt m i)     ≡⟨ [,-]-cong ([,]-∘ ((X ++ Y) ++ Z) ∘ splitAt n) (splitAt m i) ⟩
-    [ X , [ (_ ++ Z) ∘ i₁ ∘ i₂ {m} , _ ]′ ∘ splitAt n ]′ (splitAt m i)  ≡⟨ [,-]-cong ([-,]-cong (++-↑ˡ (X ++ Y) Z ∘ i₂) ∘ splitAt n) (splitAt m i) ⟩
-    [ X , [ (X ++ Y) ∘ i₂ , _ ]′ ∘ splitAt n ]′ (splitAt m i)           ≡⟨ [,-]-cong ([-,]-cong (++-↑ʳ X Y) ∘ splitAt n) (splitAt m i) ⟩
-    [ X , [ Y , ((X ++ Y) ++ Z) ∘ i₂ ]′ ∘ splitAt n ]′ (splitAt m i)    ≡⟨ [,-]-cong ([,-]-cong (++-↑ʳ (X ++ Y) Z) ∘ splitAt n) (splitAt m i) ⟩
-    [ X , [ Y , Z ]′ ∘ splitAt n ]′ (splitAt m i)                       ≡⟨⟩
-    (X ++ (Y ++ Z)) i                                                   ∎
-  where
-    open Bool
-    open Fin
-    open ≡-Reasoning
-
--- TODO also Data.Vector
-Pull-unitaryˡ
-    : {n : ℕ}
-      (X : ∣ Values n ∣)
-    → (X ++ []) ∘ i₁ ≗ X
-Pull-unitaryˡ {n} X i = begin
-    [ X , [] ]′ (splitAt _ (i ↑ˡ 0))  ≡⟨ ≡.cong ([ X , [] ]′) (splitAt-↑ˡ n i 0) ⟩
-    [ X , [] ]′ (inj₁ i)              ≡⟨⟩
-    X i                               ∎
-  where
-    open ≡-Reasoning
-
-open import Function.Bundles using (Inverse)
-open import Categories.Category.Instance.Nat using (Nat)
-open import Categories.Morphism Nat using (_≅_)
-Pull-swap
-    : {n m : ℕ}
-      (X : ∣ Values n ∣)
-      (Y : ∣ Values m ∣)
-    → (X ++ Y) ∘ (+-swap {n}) ≗ Y ++ X
-Pull-swap {n} {m} X Y i = begin
-    ((X ++ Y) ∘ +-swap {n}) i                         ≡⟨ [,]-∘ (X ++ Y) (splitAt m i) ⟩
-    [ (X ++ Y) ∘ i₂ , (X ++ Y) ∘ i₁ ]′ (splitAt m i)  ≡⟨ [-,]-cong (++-↑ʳ X Y) (splitAt m i) ⟩
-    [ Y , (X ++ Y) ∘ i₁ ]′ (splitAt m i)              ≡⟨ [,-]-cong (++-↑ˡ X Y) (splitAt m i) ⟩
-    [ Y , X ]′ (splitAt m i)                          ≡⟨⟩
-    (Y ++ X) i                                        ∎
-  where
-    open ≡-Reasoning
-    open Inverse
-    module +-swap = _≅_ (+-comm {m} {n})
-    n+m↔m+n : Permutation (n + m) (m + n)
-    n+m↔m+n .to = +-swap.to
-    n+m↔m+n .from = +-swap.from
-    n+m↔m+n .to-cong ≡.refl = ≡.refl
-    n+m↔m+n .from-cong ≡.refl = ≡.refl
-    n+m↔m+n .inverse = (λ { ≡.refl → +-swap.isoˡ _ }) , (λ { ≡.refl → +-swap.isoʳ _ })
+  isoʳ (iso Pull-ε) {x} = []-unique [] x
+
+  opaque
+    unfolding _++_
+    unfolding Pull-defs
+    Pull-++
+        : {n n′ m m′ : ℕ}
+          (f : Fin n → Fin n′)
+          (g : Fin m → Fin m′)
+          {xs : ∣ Values n′ ∣}
+          {ys : ∣ Values m′ ∣}
+        → (Pull.₁ f ⟨$⟩ xs) ++ (Pull.₁ g ⟨$⟩ ys) ≋ Pull.₁ (f +₁ g) ⟨$⟩ (xs ++ ys)
+    Pull-++ {n} {n′} {m} {m′} f g {xs} {ys} e = begin
+        (xs ∘ f ++ ys ∘ g) e                            ≡⟨ [,]-map (splitAt n e) ⟨
+        [ xs , ys ]′ (map f g (splitAt n e))            ≡⟨ ≡.cong [ xs , ys ]′ (splitAt-join n′ m′ (map f g (splitAt n e))) ⟨
+        (xs ++ ys) (join n′ m′ (map f g (splitAt n e))) ≡⟨ ≡.cong (xs ++ ys) ([,]-map (splitAt n e)) ⟩
+        (xs ++ ys) ((f +₁ g) e)                         ∎
+
+  module _ {n m : ℕ} where
+
+    opaque
+      unfolding splitₛ
+
+      open import Function.Construct.Setoid using (setoid)
+      open module ⇒ₛ {A} {B} = Setoid (setoid {0ℓ} {0ℓ} {0ℓ} {0ℓ} A B) using (_≈_)
+      open import Function.Construct.Setoid using (_∙_)
+      open import Function.Construct.Identity using () renaming (function to Id)
+
+      split∘++ : splitₛ ∙ ++ₛ ≈ Id (Values n ×ₛ Values m)
+      split∘++ {xs , ys} .proj₁ i = ≡.cong [ xs , ys ]′ (splitAt-↑ˡ n i m)
+      split∘++ {xs , ys} .proj₂ i = ≡.cong [ xs , ys ]′ (splitAt-↑ʳ n m i)
+
+      ++∘split : ++ₛ {n} ∙ splitₛ ≈ Id (Values (n + m))
+      ++∘split {x} i = ≡.trans (≡.sym ([,]-∘ x (splitAt n i))) (≡.cong x (join-splitAt n m i))
+
+  ⊗-homomorphism : NaturalIsomorphism (-×- ∘F (Pull ⁂ Pull)) (Pull ∘F -+-)
+  ⊗-homomorphism = niHelper record
+      { η = λ (n , m) → ++ₛ {n} {m}
+      ; η⁻¹ = λ (n , m) → splitₛ {n} {m}
+      ; commute = λ { {n , m} {n′ , m′} (f , g) {xs , ys} → Pull-++ f  g }
+      ; iso = λ (n , m) → record
+          { isoˡ = split∘++
+          ; isoʳ = ++∘split
+          }
+      }
+
+  module _ {n m : ℕ} where
+
+    opaque
+      unfolding Pull-++
+
+      Pull-i₁
+          : (X : ∣ Values n ∣)
+            (Y : ∣ Values m ∣)
+          → Pull.₁ i₁ ⟨$⟩ (X ++ Y) ≋ X
+      Pull-i₁ X Y i = ≡.cong [ X , Y ]′ (splitAt-↑ˡ n i m)
+
+      Pull-i₂
+          : (X : ∣ Values n ∣)
+            (Y : ∣ Values m ∣)
+          → Pull.₁ i₂ ⟨$⟩ (X ++ Y) ≋ Y
+      Pull-i₂ X Y i = ≡.cong [ X , Y ]′ (splitAt-↑ʳ n m i)
+
+  opaque
+    unfolding Pull-++
+
+    Push-assoc
+        : {m n o : ℕ}
+          (X : ∣ Values m ∣)
+          (Y : ∣ Values n ∣)
+          (Z : ∣ Values o ∣)
+        → Pull.₁ (+-assocʳ {m} {n} {o}) ⟨$⟩ ((X ++ Y) ++ Z) ≋ X ++ (Y ++ Z)
+    Push-assoc {m} {n} {o} X Y Z i = ++-assoc X Y Z i
+
+    Pull-swap
+        : {n m : ℕ}
+          (X : ∣ Values n ∣)
+          (Y : ∣ Values m ∣)
+        → Pull.₁ (+-swap {n}) ⟨$⟩ (X ++ Y) ≋ Y ++ X
+    Pull-swap {n} {m} X Y i = begin
+        ((X ++ Y) ∘ +-swap {n}) i                         ≡⟨ [,]-∘ (X ++ Y) (splitAt m i) ⟩
+        [ (X ++ Y) ∘ i₂ , (X ++ Y) ∘ i₁ ]′ (splitAt m i)  ≡⟨ [-,]-cong (Pull-i₂ X Y) (splitAt m i) ⟩
+        [ Y , (X ++ Y) ∘ i₁ ]′ (splitAt m i)              ≡⟨ [,-]-cong (Pull-i₁ X Y) (splitAt m i) ⟩
+        [ Y , X ]′ (splitAt m i)                          ≡⟨⟩
+        (Y ++ X) i                                        ∎
 
 open SymmetricMonoidalFunctor
+
 Pull,++,[] : SymmetricMonoidalFunctor
 Pull,++,[] .F = Pull
 Pull,++,[] .isBraidedMonoidal = record
     { isStrongMonoidal = record
         { ε = Pull-ε
         ; ⊗-homo = ⊗-homomorphism
-        ; associativity = λ { {m} {n} {o} {(X , Y) , Z} i → ++-assoc X Y Z i  }
-        ; unitaryˡ = λ _ → ≡.refl
-        ; unitaryʳ = λ { {n} {X , _} i → Pull-unitaryˡ X i }
+        ; associativity = λ { {_} {_} {_} {(X , Y) , Z} → Push-assoc X Y Z }
+        ; unitaryˡ = λ { {n} {_ , X} → Pull-i₂ {0} {n} [] X }
+        ; unitaryʳ = λ { {n} {X , _} → Pull-i₁ {n} {0} X [] }
         }
-    ; braiding-compat = λ { {n} {m} {X , Y} i → Pull-swap X Y i }
+    ; braiding-compat = λ { {n} {m} {X , Y} → Pull-swap X Y }
     }
+
+module Pull,++,[] = SymmetricMonoidalFunctor Pull,++,[]
diff --git a/Functor/Monoidal/Instance/Nat/Push.agda b/Functor/Monoidal/Instance/Nat/Push.agda
index 667d68e..b53282d 100644
--- a/Functor/Monoidal/Instance/Nat/Push.agda
+++ b/Functor/Monoidal/Instance/Nat/Push.agda
@@ -9,12 +9,14 @@ open import Function.Base using (_∘_; case_of_; _$_; id)
 open import Function.Bundles using (Func; _⟶ₛ_; _⟨$⟩_)
 open import Level using (0ℓ; Level)
 open import Relation.Binary using (Rel; Setoid)
-open import Functor.Instance.Nat.Push using (Push; Push₁; Push-identity)
-open import Categories.Category.Instance.SingletonSet using (SingletonSetoid)
+open import Functor.Instance.Nat.Push using (Push; Push-defs)
+open import Categories.Category.Instance.SingletonSet using () renaming (SingletonSetoid to ⊤ₛ)
 open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper)
-open import Data.Vec.Functional using (Vector; []; _++_; head; tail)
-open import Data.Vec.Functional.Properties using (++-cong)
+open import Data.Vec.Functional as Vec using (Vector)
+open import Data.Vector using (++-assoc; ++-↑ˡ; ++-↑ʳ)
+-- open import Data.Vec.Functional.Properties using (++-cong)
 open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-Cartesian)
+open import Function.Construct.Constant using () renaming (function to Const)
 open import Categories.Category.BinaryProducts using (module BinaryProducts)
 open import Categories.Category.Cartesian using (Cartesian)
 open Cartesian (Setoids-Cartesian {0ℓ} {0ℓ}) using (products)
@@ -25,17 +27,17 @@ open import Categories.Category.Product using (_⁂_)
 open import Categories.Functor using () renaming (_∘F_ to _∘′_)
 open Cocartesian Nat-Cocartesian using (module Dual; i₁; i₂; -+-; _+₁_; +-assoc; +-assocʳ; +-assocˡ; +-comm; +-swap; +₁∘+-swap)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
-open import Data.Nat.Base using (ℕ; _+_)
-open import Data.Fin.Base using (Fin)
+open import Data.Nat using (ℕ; _+_)
+open import Data.Fin using (Fin)
 open import Data.Product.Base using (_,_; _×_; Σ)
 open import Data.Fin.Preimage using (preimage; preimage-⊥; preimage-cong₂)
 open import Functor.Monoidal.Instance.Nat.Preimage using (preimage-++)
 open import Data.Sum.Base using ([_,_]; [_,_]′; inj₁; inj₂)
 open import Data.Sum.Properties using ([,]-cong; [,-]-cong; [-,]-cong; [,]-∘; [,]-map)
-open import Data.Circuit.Merge using (merge-with; merge; merge-⊥; merge-[]; merge-cong₁; merge-cong₂; merge-suc; _when_; join-merge; merge-preimage-ρ; merge-⁅⁆)
-open import Data.Circuit.Value using (Value; join; join-comm; join-assoc)
+open import Data.Circuit.Merge using (merge-with; merge; merge-⊥; merge-[]; ⁅⁆-++; merge-++; merge-cong₁; merge-cong₂; merge-suc; _when_; join-merge; merge-preimage-ρ; merge-⁅⁆)
+open import Data.Circuit.Value using (Value; join; join-comm; join-assoc; Monoid)
 open import Data.Fin.Base using (splitAt; _↑ˡ_; _↑ʳ_) renaming (join to joinAt)
-open import Data.Fin.Properties using (splitAt-↑ˡ; splitAt-↑ʳ; splitAt⁻¹-↑ˡ; splitAt⁻¹-↑ʳ; ↑ˡ-injective; ↑ʳ-injective; _≟_; 2↔Bool)
+open import Data.Fin.Properties using (splitAt-↑ˡ; splitAt-↑ʳ; splitAt⁻¹-↑ˡ; splitAt⁻¹-↑ʳ; ↑ˡ-injective; ↑ʳ-injective; _≟_)
 open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≢_; _≗_; module ≡-Reasoning)
 open BinaryProducts products using (-×-)
 open Value using (U)
@@ -51,278 +53,144 @@ open import Function.Bundles using (Inverse)
 open import Data.Fin.Permutation using (Permutation; _⟨$⟩ʳ_; _⟨$⟩ˡ_)
 open Dual.op-binaryProducts using () renaming (assocˡ∘⟨⟩ to []∘assocʳ; swap∘⟨⟩ to []∘swap)
 open import Relation.Nullary.Decidable using (does; does-⇔; dec-false)
-
-open import Data.System.Values Value using (Values)
-
-open Func
-Push-ε : SingletonSetoid {0ℓ} {0ℓ} ⟶ₛ Values 0
-to Push-ε x = []
-cong Push-ε x ()
-
-++ₛ : {n m : ℕ} → Values n ×ₛ Values m ⟶ₛ Values (n + m)
-to ++ₛ (xs , ys) = xs ++ ys
-cong ++ₛ (≗xs , ≗ys) = ++-cong _ _ ≗xs ≗ys
-
-∣_∣ : {c ℓ : Level} → Setoid c ℓ → Set c
-∣_∣ = Setoid.Carrier
+open import Data.Setoid using (∣_∣)
 
 open ℕ
-merge-++
-    : {n m : ℕ}
-      (xs : ∣ Values n ∣)
-      (ys : ∣ Values m ∣)
-      (S₁ : Subset n)
-      (S₂ : Subset m)
-    → merge (xs ++ ys) (S₁ ++ S₂)
-    ≡ join (merge xs S₁) (merge ys S₂)
-merge-++ {zero} {m} xs ys S₁ S₂ = begin
-    merge (xs ++ ys) (S₁ ++ S₂)       ≡⟨ merge-cong₂ (xs ++ ys) (λ _ → ≡.refl) ⟩
-    merge (xs ++ ys) S₂               ≡⟨ merge-cong₁ (λ _ → ≡.refl) S₂ ⟩
-    merge ys S₂                       ≡⟨ ≡.cong (λ h → join h (merge ys S₂)) (merge-[] xs S₁) ⟨
-    join (merge xs S₁) (merge ys S₂)  ∎
-  where
-    open ≡-Reasoning
-merge-++ {suc n} {m} xs ys S₁ S₂ = begin
-    merge (xs ++ ys) (S₁ ++ S₂)                                                   ≡⟨ merge-suc (xs ++ ys) (S₁ ++ S₂) ⟩
-    merge-with (head xs when head S₁) (tail (xs ++ ys)) (tail (S₁ ++ S₂))         ≡⟨ join-merge (head xs when head S₁) (tail (xs ++ ys)) (tail (S₁ ++ S₂)) ⟨
-    join (head xs when head S₁) (merge (tail (xs ++ ys)) (tail (S₁ ++ S₂)))
-        ≡⟨ ≡.cong (join (head xs when head S₁)) (merge-cong₁ ([,]-map ∘ splitAt n) (tail (S₁ ++ S₂))) ⟩
-    join (head xs when head S₁) (merge (tail xs ++ ys) (tail (S₁ ++ S₂)))
-        ≡⟨ ≡.cong (join (head xs when head S₁)) (merge-cong₂ (tail xs ++ ys) ([,]-map ∘ splitAt n)) ⟩
-    join (head xs when head S₁) (merge (tail xs ++ ys) (tail S₁ ++ S₂))           ≡⟨ ≡.cong (join (head xs when head S₁)) (merge-++ (tail xs) ys (tail S₁) S₂) ⟩
-    join (head xs when head S₁) (join (merge (tail xs) (tail S₁)) (merge ys S₂))  ≡⟨ join-assoc (head xs when head S₁) (merge (tail xs) (tail S₁)) _ ⟨
-    join (join (head xs when head S₁) (merge (tail xs) (tail S₁))) (merge ys S₂)
-        ≡⟨ ≡.cong (λ h → join h (merge ys S₂)) (join-merge (head xs when head S₁) (tail xs) (tail S₁)) ⟩
-    join (merge-with (head xs when head S₁) (tail xs) (tail S₁)) (merge ys S₂)    ≡⟨ ≡.cong (λ h → join h (merge ys S₂)) (merge-suc xs S₁) ⟨
-    join (merge xs S₁) (merge ys S₂)                                              ∎
-  where
-    open ≡-Reasoning
-
-open Fin
-⁅⁆-≟ : {n : ℕ} (x y : Fin n) → ⁅ x ⁆ y ≡ does (x ≟ y)
-⁅⁆-≟ zero zero = ≡.refl
-⁅⁆-≟ zero (suc y) = ≡.refl
-⁅⁆-≟ (suc x) zero = ≡.refl
-⁅⁆-≟ (suc x) (suc y) = ⁅⁆-≟ x y
 
-Push-++
-    : {n n′ m m′ : ℕ}
-      (f : Fin n → Fin n′)
-      (g : Fin m → Fin m′)
-      (xs : ∣ Values n ∣)
-      (ys : ∣ Values m ∣)
-    → merge xs ∘ preimage f ∘ ⁅_⁆ ++ merge ys ∘ preimage g ∘ ⁅_⁆
-    ≗ merge (xs ++ ys) ∘ preimage (f +₁ g) ∘ ⁅_⁆
-Push-++ {n} {n′} {m} {m′} f g xs ys i = begin
-    ((merge xs ∘ preimage f ∘ ⁅_⁆) ++ (merge ys ∘ preimage g ∘ ⁅_⁆)) i ≡⟨⟩
-    [ merge xs ∘ preimage f ∘ ⁅_⁆ , merge ys ∘ preimage g ∘ ⁅_⁆ ]′ (splitAt n′ i)
-        ≡⟨ [,]-cong left right (splitAt n′ i) ⟩
-    [ (λ x → merge (xs ++ ys) _) , (λ x → merge (xs ++ ys) _) ]′ (splitAt n′ i)
-        ≡⟨ [,]-∘ (merge (xs ++ ys) ∘ (preimage (f +₁ g))) (splitAt n′ i) ⟨
-    merge (xs ++ ys) (preimage (f +₁ g) ([ ⁅⁆++⊥ , ⊥++⁅⁆ ]′ (splitAt n′ i))) ≡⟨⟩
-    merge (xs ++ ys) (preimage (f +₁ g) ((⁅⁆++⊥ ++ ⊥++⁅⁆) i)) ≡⟨ merge-cong₂ (xs ++ ys) (preimage-cong₂ (f +₁ g) (⁅⁆-++ i)) ⟩
-    merge (xs ++ ys) (preimage (f +₁ g) ⁅ i ⁆) ∎
-  where
-    open ≡-Reasoning
-    left : (x : Fin n′) → merge xs (preimage f ⁅ x ⁆) ≡ merge (xs ++ ys) (preimage (f +₁ g) (⁅ x ⁆ ++ ⊥))
-    left x = begin
-        merge xs (preimage f ⁅ x ⁆)                                   ≡⟨ join-comm U (merge xs (preimage f ⁅ x ⁆)) ⟩
-        join (merge xs (preimage f ⁅ x ⁆)) U                          ≡⟨ ≡.cong (join (merge _ _)) (merge-⊥ ys) ⟨
-        join (merge xs (preimage f ⁅ x ⁆)) (merge ys ⊥)               ≡⟨ ≡.cong (join (merge _ _)) (merge-cong₂ ys (preimage-⊥ g)) ⟨
-        join (merge xs (preimage f ⁅ x ⁆)) (merge ys (preimage g ⊥))  ≡⟨ merge-++ xs ys (preimage f ⁅ x ⁆) (preimage g ⊥) ⟨
-        merge (xs ++ ys) ((preimage f ⁅ x ⁆) ++ (preimage g ⊥))       ≡⟨ merge-cong₂ (xs ++ ys) (preimage-++ f g) ⟩
-        merge (xs ++ ys) (preimage (f +₁ g) (⁅ x ⁆ ++ ⊥))             ∎
-    right : (x : Fin m′) → merge ys (preimage g ⁅ x ⁆) ≡ merge (xs ++ ys) (preimage (f +₁ g) (⊥ ++ ⁅ x ⁆))
-    right x = begin
-        merge ys (preimage g ⁅ x ⁆)                                   ≡⟨⟩
-        join U (merge ys (preimage g ⁅ x ⁆))                          ≡⟨ ≡.cong (λ h → join h (merge _ _)) (merge-⊥ xs) ⟨
-        join (merge xs ⊥) (merge ys (preimage g ⁅ x ⁆))               ≡⟨ ≡.cong (λ h → join h (merge _ _)) (merge-cong₂ xs (preimage-⊥ f)) ⟨
-        join (merge xs (preimage f ⊥)) (merge ys (preimage g ⁅ x ⁆))  ≡⟨ merge-++ xs ys (preimage f ⊥) (preimage g ⁅ x ⁆) ⟨
-        merge (xs ++ ys) ((preimage f ⊥) ++ (preimage g ⁅ x ⁆))       ≡⟨ merge-cong₂ (xs ++ ys) (preimage-++ f g) ⟩
-        merge (xs ++ ys) (preimage (f +₁ g) (⊥ ++ ⁅ x ⁆))             ∎
-    ⁅⁆++⊥ : Vector (Subset (n′ + m′)) n′
-    ⁅⁆++⊥ x = ⁅ x ⁆ ++ ⊥
-    ⊥++⁅⁆ : Vector (Subset (n′ + m′)) m′
-    ⊥++⁅⁆ x = ⊥ ++ ⁅ x ⁆
+open import Data.System.Values Monoid using (Values; <ε>; ++ₛ; _++_; head; tail; _≋_)
 
-    open ℕ
-
-    open Equivalence
-
-    ⁅⁆-++
-        : (i : Fin (n′ + m′))
-        → [ (λ x → ⁅ x ⁆ ++ ⊥) , (λ x → ⊥ ++ ⁅ x ⁆) ]′ (splitAt n′ i) ≗ ⁅ i ⁆
-    ⁅⁆-++ i x with splitAt n′ i in eq₁
-    ... | inj₁ i′ with splitAt n′ x in eq₂
-    ...   | inj₁ x′ = begin
-                ⁅ i′ ⁆ x′                   ≡⟨ ⁅⁆-≟ i′ x′ ⟩
-                does (i′ ≟ x′)              ≡⟨ does-⇔ ⇔ (i′ ≟ x′) (i′ ↑ˡ m′ ≟ x′ ↑ˡ m′) ⟩
-                does (i′ ↑ˡ m′ ≟ x′ ↑ˡ m′)  ≡⟨ ⁅⁆-≟ (i′ ↑ˡ m′) (x′ ↑ˡ m′) ⟨
-                ⁅ i′ ↑ˡ m′ ⁆ (x′ ↑ˡ m′)     ≡⟨ ≡.cong₂ ⁅_⁆ (splitAt⁻¹-↑ˡ eq₁) (splitAt⁻¹-↑ˡ eq₂) ⟩
-                ⁅ i ⁆ x                 ∎
-              where
-                ⇔ : Equivalence (≡.setoid (i′ ≡ x′)) (≡.setoid (i′ ↑ˡ m′ ≡ x′ ↑ˡ m′))
-                ⇔ .to = ≡.cong (_↑ˡ m′)
-                ⇔ .from = ↑ˡ-injective m′ i′ x′
-                ⇔ .to-cong ≡.refl = ≡.refl
-                ⇔ .from-cong ≡.refl = ≡.refl
-    ...   | inj₂ x′ = begin
-                false                       ≡⟨ dec-false (i′ ↑ˡ m′ ≟ n′ ↑ʳ x′) ↑ˡ≢↑ʳ ⟨
-                does (i′ ↑ˡ m′ ≟ n′ ↑ʳ x′)  ≡⟨ ⁅⁆-≟ (i′ ↑ˡ m′) (n′ ↑ʳ x′) ⟨
-                ⁅ i′ ↑ˡ m′ ⁆ (n′ ↑ʳ x′)     ≡⟨ ≡.cong₂ ⁅_⁆ (splitAt⁻¹-↑ˡ eq₁) (splitAt⁻¹-↑ʳ eq₂) ⟩
-                ⁅ i ⁆ x                     ∎
-              where
-                ↑ˡ≢↑ʳ : i′ ↑ˡ m′ ≢ n′ ↑ʳ x′
-                ↑ˡ≢↑ʳ ≡ = case ≡.trans (≡.sym (splitAt-↑ˡ n′ i′ m′)) (≡.trans (≡.cong (splitAt n′) ≡) (splitAt-↑ʳ n′ m′ x′)) of λ { () }
-    ⁅⁆-++ i x | inj₂ i′ with splitAt n′ x in eq₂
-    ⁅⁆-++ i x | inj₂ i′ | inj₁ x′ = ≡.trans (≡.cong ([ ⊥ , ⁅ i′ ⁆ ]′) eq₂) $ begin
-        false                       ≡⟨ dec-false (n′ ↑ʳ i′ ≟ x′ ↑ˡ m′) ↑ʳ≢↑ˡ ⟨
-        does (n′ ↑ʳ i′ ≟ x′ ↑ˡ m′)  ≡⟨ ⁅⁆-≟ (n′ ↑ʳ i′) (x′ ↑ˡ m′) ⟨
-        ⁅ n′ ↑ʳ i′ ⁆ (x′ ↑ˡ m′)     ≡⟨ ≡.cong₂ ⁅_⁆ (splitAt⁻¹-↑ʳ eq₁) (splitAt⁻¹-↑ˡ eq₂) ⟩
-        ⁅ i ⁆ x                     ∎
+open Func
+open ≡-Reasoning
+
+private
+
+  Push-ε : ⊤ₛ {0ℓ} {0ℓ} ⟶ₛ Values 0
+  Push-ε = Const ⊤ₛ (Values 0) <ε>
+
+  opaque
+
+    unfolding _++_
+
+    unfolding Push-defs
+    Push-++
+        : {n n′ m m′ : ℕ }
+        → (f : Fin n → Fin n′)
+        → (g : Fin m → Fin m′)
+        → (xs : ∣ Values n ∣)
+        → (ys : ∣ Values m ∣)
+        → (Push.₁ f ⟨$⟩ xs) ++ (Push.₁ g ⟨$⟩ ys)
+        ≋ Push.₁ (f +₁ g) ⟨$⟩ (xs ++ ys)
+    Push-++ {n} {n′} {m} {m′} f g xs ys i = begin
+        ((merge xs ∘ preimage f ∘ ⁅_⁆) ++ (merge ys ∘ preimage g ∘ ⁅_⁆)) i
+            ≡⟨ [,]-cong left right (splitAt n′ i) ⟩
+        [ (λ x → merge (xs ++ ys) _) , (λ x → merge (xs ++ ys) _) ]′ (splitAt n′ i)
+            ≡⟨ [,]-∘ (merge (xs ++ ys) ∘ (preimage (f +₁ g))) (splitAt n′ i) ⟨
+        merge (xs ++ ys) (preimage (f +₁ g) ((⁅⁆++⊥ Vec.++ ⊥++⁅⁆) i))     ≡⟨ merge-cong₂ (xs ++ ys) (preimage-cong₂ (f +₁ g) (⁅⁆-++ {n′} i)) ⟩
+        merge (xs ++ ys) (preimage (f +₁ g) ⁅ i ⁆) ∎
       where
-        ↑ʳ≢↑ˡ : n′ ↑ʳ i′ ≢ x′ ↑ˡ m′
-        ↑ʳ≢↑ˡ ≡ = case ≡.trans (≡.sym (splitAt-↑ʳ n′ m′ i′)) (≡.trans (≡.cong (splitAt n′) ≡) (splitAt-↑ˡ n′ x′ m′)) of λ { () }
-    ⁅⁆-++ i x | inj₂ i′ | inj₂ x′ = begin
-        [ ⊥ , ⁅ i′ ⁆ ] (splitAt n′ x) ≡⟨ ≡.cong ([ ⊥ , ⁅ i′ ⁆ ]) eq₂ ⟩
-        ⁅ i′ ⁆ x′                     ≡⟨ ⁅⁆-≟ i′ x′ ⟩
-        does (i′ ≟ x′)                ≡⟨ does-⇔ ⇔ (i′ ≟ x′) (n′ ↑ʳ i′ ≟ n′ ↑ʳ x′) ⟩
-        does (n′ ↑ʳ i′ ≟ n′ ↑ʳ x′)    ≡⟨ ⁅⁆-≟ (n′ ↑ʳ i′) (n′ ↑ʳ x′) ⟨
-        ⁅ n′ ↑ʳ i′ ⁆ (n′ ↑ʳ x′)       ≡⟨ ≡.cong₂ ⁅_⁆ (splitAt⁻¹-↑ʳ eq₁) (splitAt⁻¹-↑ʳ eq₂) ⟩
-        ⁅ i ⁆ x                       ∎
+        ⁅⁆++⊥ : Vector (Subset (n′ + m′)) n′
+        ⁅⁆++⊥ x = ⁅ x ⁆ Vec.++ ⊥
+        ⊥++⁅⁆ : Vector (Subset (n′ + m′)) m′
+        ⊥++⁅⁆ x = ⊥ Vec.++ ⁅ x ⁆
+        left : (x : Fin n′) → merge xs (preimage f ⁅ x ⁆) ≡ merge (xs ++ ys) (preimage (f +₁ g) (⁅ x ⁆ Vec.++ ⊥))
+        left x = begin
+            merge xs (preimage f ⁅ x ⁆)                                   ≡⟨ join-comm U (merge xs (preimage f ⁅ x ⁆)) ⟩
+            join (merge xs (preimage f ⁅ x ⁆)) U                          ≡⟨ ≡.cong (join (merge _ _)) (merge-⊥ ys) ⟨
+            join (merge xs (preimage f ⁅ x ⁆)) (merge ys ⊥)               ≡⟨ ≡.cong (join (merge _ _)) (merge-cong₂ ys (preimage-⊥ g)) ⟨
+            join (merge xs (preimage f ⁅ x ⁆)) (merge ys (preimage g ⊥))  ≡⟨ merge-++ xs ys (preimage f ⁅ x ⁆) (preimage g ⊥) ⟨
+            merge (xs ++ ys) ((preimage f ⁅ x ⁆) Vec.++ (preimage g ⊥))   ≡⟨ merge-cong₂ (xs ++ ys) (preimage-++ f g) ⟩
+            merge (xs ++ ys) (preimage (f +₁ g) (⁅ x ⁆ Vec.++ ⊥))         ∎
+        right : (x : Fin m′) → merge ys (preimage g ⁅ x ⁆) ≡ merge (xs ++ ys) (preimage (f +₁ g) (⊥ Vec.++ ⁅ x ⁆))
+        right x = begin
+            merge ys (preimage g ⁅ x ⁆)                                   ≡⟨⟩
+            join U (merge ys (preimage g ⁅ x ⁆))                          ≡⟨ ≡.cong (λ h → join h (merge _ _)) (merge-⊥ xs) ⟨
+            join (merge xs ⊥) (merge ys (preimage g ⁅ x ⁆))               ≡⟨ ≡.cong (λ h → join h (merge _ _)) (merge-cong₂ xs (preimage-⊥ f)) ⟨
+            join (merge xs (preimage f ⊥)) (merge ys (preimage g ⁅ x ⁆))  ≡⟨ merge-++ xs ys (preimage f ⊥) (preimage g ⁅ x ⁆) ⟨
+            merge (xs ++ ys) ((preimage f ⊥) Vec.++ (preimage g ⁅ x ⁆))   ≡⟨ merge-cong₂ (xs ++ ys) (preimage-++ f g) ⟩
+            merge (xs ++ ys) (preimage (f +₁ g) (⊥ Vec.++ ⁅ x ⁆))         ∎
+
+  ⊗-homomorphism : NaturalTransformation (-×- ∘′ (Push ⁂ Push)) (Push ∘′ -+-)
+  ⊗-homomorphism = ntHelper record
+      { η = λ (n , m) → ++ₛ {n} {m}
+      ; commute = λ { (f , g) {xs , ys} → Push-++ f g xs ys }
+      }
+
+  opaque
+
+    unfolding Push-defs
+    unfolding _++_
+
+    Push-assoc
+        : {m n o : ℕ}
+          (X : ∣ Values m ∣)
+          (Y : ∣ Values n ∣)
+          (Z : ∣ Values o ∣)
+        → (Push.₁ (+-assocˡ {m} {n} {o}) ⟨$⟩ ((X ++ Y) ++ Z)) ≋ X ++ Y ++ Z
+    Push-assoc {m} {n} {o} X Y Z i = begin
+        merge ((X ++ Y) ++ Z) (preimage (+-assocˡ {m}) ⁅ i ⁆)         ≡⟨ merge-preimage-ρ ↔-mno ((X ++ Y) ++ Z) ⁅ i ⁆ ⟩
+        merge (((X ++ Y) ++ Z) ∘ (+-assocʳ {m})) (⁅ i ⁆)              ≡⟨⟩
+        merge (((X ++ Y) ++ Z) ∘ (+-assocʳ {m})) (preimage id ⁅ i ⁆)  ≡⟨ merge-cong₁ (++-assoc X Y Z) (preimage id ⁅ i ⁆) ⟩
+        merge (X ++ (Y ++ Z)) (preimage id ⁅ i ⁆)                     ≡⟨ Push.identity i ⟩
+        (X ++ (Y ++ Z)) i                                             ∎
       where
-        ⇔ : Equivalence (≡.setoid (i′ ≡ x′)) (≡.setoid (n′ ↑ʳ i′ ≡ n′ ↑ʳ x′))
-        ⇔ .to = ≡.cong (n′ ↑ʳ_)
-        ⇔ .from = ↑ʳ-injective n′ i′ x′
-        ⇔ .to-cong ≡.refl = ≡.refl
-        ⇔ .from-cong ≡.refl = ≡.refl
-
-⊗-homomorphism : NaturalTransformation (-×- ∘′ (Push ⁂ Push)) (Push ∘′ -+-)
-⊗-homomorphism = ntHelper record
-    { η = λ (n , m) → ++ₛ {n} {m}
-    ; commute = λ { {n , m} {n′ , m′} (f , g) {xs , ys} i → Push-++ f g xs ys i }
-    }
-
-++-↑ˡ
-    : {n m : ℕ}
-      (X : ∣ Values n ∣)
-      (Y : ∣ Values m ∣)
-    → (X ++ Y) ∘ i₁ ≗ X
-++-↑ˡ {n} {m} X Y i = ≡.cong [ X , Y ]′ (splitAt-↑ˡ n i m)
-
-++-↑ʳ
-    : {n m : ℕ}
-      (X : ∣ Values n ∣)
-      (Y : ∣ Values m ∣)
-    → (X ++ Y) ∘ i₂ ≗ Y
-++-↑ʳ {n} {m} X Y i = ≡.cong [ X , Y ]′ (splitAt-↑ʳ n m i)
-
-++-assoc
-    : {m n o : ℕ}
-      (X : ∣ Values m ∣)
-      (Y : ∣ Values n ∣)
-      (Z : ∣ Values o ∣)
-    → ((X ++ Y) ++ Z) ∘ +-assocʳ {m} ≗ X ++ (Y ++ Z)
-++-assoc {m} {n} {o} X Y Z i = begin
-    ((X ++ Y) ++ Z) (+-assocʳ {m} i)                                    ≡⟨⟩
-    ((X ++ Y) ++ Z) ([ i₁ ∘ i₁ , _ ]′ (splitAt m i))                    ≡⟨ [,]-∘ ((X ++ Y) ++ Z) (splitAt m i) ⟩
-    [ ((X ++ Y) ++ Z) ∘ i₁ ∘ i₁ , _ ]′ (splitAt m i)                    ≡⟨ [-,]-cong (++-↑ˡ (X ++ Y) Z ∘ i₁) (splitAt m i) ⟩
-    [ (X ++ Y) ∘ i₁ , _ ]′ (splitAt m i)                                ≡⟨ [-,]-cong (++-↑ˡ X Y) (splitAt m i) ⟩
-    [ X , ((X ++ Y) ++ Z) ∘ [ _ , _ ]′ ∘ splitAt n ]′ (splitAt m i)     ≡⟨ [,-]-cong ([,]-∘ ((X ++ Y) ++ Z) ∘ splitAt n) (splitAt m i) ⟩
-    [ X , [ (_ ++ Z) ∘ i₁ ∘ i₂ {m} , _ ]′ ∘ splitAt n ]′ (splitAt m i)  ≡⟨ [,-]-cong ([-,]-cong (++-↑ˡ (X ++ Y) Z ∘ i₂) ∘ splitAt n) (splitAt m i) ⟩
-    [ X , [ (X ++ Y) ∘ i₂ , _ ]′ ∘ splitAt n ]′ (splitAt m i)           ≡⟨ [,-]-cong ([-,]-cong (++-↑ʳ X Y) ∘ splitAt n) (splitAt m i) ⟩
-    [ X , [ Y , ((X ++ Y) ++ Z) ∘ i₂ ]′ ∘ splitAt n ]′ (splitAt m i)    ≡⟨ [,-]-cong ([,-]-cong (++-↑ʳ (X ++ Y) Z) ∘ splitAt n) (splitAt m i) ⟩
-    [ X , [ Y , Z ]′ ∘ splitAt n ]′ (splitAt m i)                       ≡⟨⟩
-    (X ++ (Y ++ Z)) i                                                   ∎
-  where
-    open Bool
-    open Fin
-    open ≡-Reasoning
-
-Preimage-unitaryˡ
-    : {n : ℕ}
-      (X : Subset n)
-    → (X ++ []) ∘ (_↑ˡ 0) ≗ X
-Preimage-unitaryˡ {n} X i = begin
-    [ X , [] ]′ (splitAt _ (i ↑ˡ 0))  ≡⟨ ≡.cong ([ X , [] ]′) (splitAt-↑ˡ n i 0) ⟩
-    [ X , [] ]′ (inj₁ i)              ≡⟨⟩
-    X i                               ∎
-  where
-    open ≡-Reasoning
-
-Push-assoc
-    : {m n o : ℕ}
-      (X : ∣ Values m ∣)
-      (Y : ∣ Values n ∣)
-      (Z : ∣ Values o ∣)
-    → merge ((X ++ Y) ++ Z) ∘ preimage (+-assocˡ {m}) ∘  ⁅_⁆
-    ≗ X ++ (Y ++ Z)
-Push-assoc {m} {n} {o} X Y Z i = begin
-    merge ((X ++ Y) ++ Z) (preimage (+-assocˡ {m}) ⁅ i ⁆)         ≡⟨ merge-preimage-ρ ↔-mno ((X ++ Y) ++ Z) ⁅ i ⁆ ⟩
-    merge (((X ++ Y) ++ Z) ∘ (+-assocʳ {m})) (⁅ i ⁆)              ≡⟨⟩
-    merge (((X ++ Y) ++ Z) ∘ (+-assocʳ {m})) (preimage id ⁅ i ⁆)  ≡⟨ merge-cong₁ (++-assoc X Y Z) (preimage id ⁅ i ⁆) ⟩
-    merge (X ++ (Y ++ Z)) (preimage id ⁅ i ⁆)                     ≡⟨ Push-identity i ⟩
-    (X ++ (Y ++ Z)) i                                             ∎
-  where
-    open Inverse
-    module +-assoc = _≅_ (+-assoc {m} {n} {o})
-    ↔-mno : Permutation ((m + n) + o) (m + (n + o))
-    ↔-mno .to = +-assocˡ {m}
-    ↔-mno .from = +-assocʳ {m}
-    ↔-mno .to-cong ≡.refl = ≡.refl
-    ↔-mno .from-cong ≡.refl = ≡.refl
-    ↔-mno .inverse = (λ { ≡.refl → +-assoc.isoˡ _ }) , λ { ≡.refl → +-assoc.isoʳ _ }
-    open ≡-Reasoning
-
-preimage-++′
-    : {n m o : ℕ}
-      (f : Vector (Fin o) n)
-      (g : Vector (Fin o) m)
-      (S : Subset o)
-    → preimage (f ++ g) S ≗ preimage f S ++ preimage g S
-preimage-++′ {n} f g S = [,]-∘ S ∘ splitAt n
-
-Push-unitaryʳ
-    : {n : ℕ}
-      (X : ∣ Values n ∣)
-      (i : Fin n)
-    → merge (X ++ []) (preimage (id ++ (λ ())) ⁅ i ⁆) ≡ X i
-Push-unitaryʳ {n} X i = begin
-    merge (X ++ []) (preimage (id ++ (λ ())) ⁅ i ⁆)               ≡⟨ merge-cong₂ (X ++ []) (preimage-++′ id (λ ()) ⁅ i ⁆) ⟩
-    merge (X ++ []) (preimage id ⁅ i ⁆ ++ preimage (λ ()) ⁅ i ⁆)  ≡⟨⟩
-    merge (X ++ []) (⁅ i ⁆ ++ preimage (λ ()) ⁅ i ⁆)              ≡⟨ merge-++ X [] ⁅ i ⁆ (preimage (λ ()) ⁅ i ⁆) ⟩
-    join (merge X ⁅ i ⁆) (merge [] (preimage (λ ()) ⁅ i ⁆))       ≡⟨ ≡.cong (join (merge X ⁅ i ⁆)) (merge-[] [] (preimage (λ ()) ⁅ i ⁆)) ⟩
-    join (merge X ⁅ i ⁆) U                                        ≡⟨ join-comm (merge X ⁅ i ⁆) U ⟩
-    merge X ⁅ i ⁆                                                 ≡⟨ merge-⁅⁆ X i ⟩
-    X i ∎
-  where
-    open ≡-Reasoning
-    t : Fin (n + 0) → Fin n
-    t = id ++ (λ ())
-
-Push-swap
-    : {n m : ℕ}
-      (X : ∣ Values n ∣)
-      (Y : ∣ Values m ∣)
-    → merge (X ++ Y) ∘ preimage (+-swap {m}) ∘ ⁅_⁆ ≗ Y ++ X
-Push-swap {n} {m} X Y i = begin
-    merge (X ++ Y) (preimage (+-swap {m}) ⁅ i ⁆)      ≡⟨ merge-preimage-ρ n+m↔m+n (X ++ Y) ⁅ i ⁆ ⟩
-    merge ((X ++ Y) ∘ +-swap {n}) ⁅ i ⁆               ≡⟨ merge-⁅⁆ ((X ++ Y) ∘ (+-swap {n})) i ⟩
-    ((X ++ Y) ∘ +-swap {n}) i                         ≡⟨ [,]-∘ (X ++ Y) (splitAt m i) ⟩
-    [ (X ++ Y) ∘ i₂ , (X ++ Y) ∘ i₁ ]′ (splitAt m i)  ≡⟨ [-,]-cong (++-↑ʳ X Y) (splitAt m i) ⟩
-    [ Y , (X ++ Y) ∘ i₁ ]′ (splitAt m i)              ≡⟨ [,-]-cong (++-↑ˡ X Y) (splitAt m i) ⟩
-    [ Y , X ]′ (splitAt m i)                          ≡⟨⟩
-    (Y ++ X) i                                        ∎
-  where
-    open ≡-Reasoning
-    open Inverse
-    module +-swap = _≅_ (+-comm {m} {n})
-    n+m↔m+n : Permutation (n + m) (m + n)
-    n+m↔m+n .to = +-swap.to
-    n+m↔m+n .from = +-swap.from
-    n+m↔m+n .to-cong ≡.refl = ≡.refl
-    n+m↔m+n .from-cong ≡.refl = ≡.refl
-    n+m↔m+n .inverse = (λ { ≡.refl → +-swap.isoˡ _ }) , (λ { ≡.refl → +-swap.isoʳ _ })
+        open Inverse
+        module +-assoc = _≅_ (+-assoc {m} {n} {o})
+        ↔-mno : Permutation ((m + n) + o) (m + (n + o))
+        ↔-mno .to = +-assocˡ {m}
+        ↔-mno .from = +-assocʳ {m}
+        ↔-mno .to-cong ≡.refl = ≡.refl
+        ↔-mno .from-cong ≡.refl = ≡.refl
+        ↔-mno .inverse = (λ { ≡.refl → +-assoc.isoˡ _ }) , λ { ≡.refl → +-assoc.isoʳ _ }
+
+    Push-unitaryˡ
+        : {n : ℕ}
+          (X : ∣ Values n ∣)
+        → Push.₁ id ⟨$⟩ (<ε> ++ X) ≋ X
+    Push-unitaryˡ = merge-⁅⁆
+
+    preimage-++′
+        : {n m o : ℕ}
+          (f : Vector (Fin o) n)
+          (g : Vector (Fin o) m)
+          (S : Subset o)
+        → preimage (f Vec.++ g) S ≗ preimage f S Vec.++ preimage g S
+    preimage-++′ {n} f g S = [,]-∘ S ∘ splitAt n
+
+    Push-unitaryʳ
+        : {n : ℕ}
+          (X : ∣ Values n ∣)
+        → Push.₁ (id Vec.++ (λ())) ⟨$⟩ (X ++ (<ε> {0})) ≋ X
+    Push-unitaryʳ {n} X i = begin
+        merge (X ++ <ε>) (preimage (id Vec.++ (λ ())) ⁅ i ⁆)     ≡⟨ merge-cong₂ (X Vec.++ <ε>) (preimage-++′ id (λ ()) ⁅ i ⁆) ⟩
+        merge (X ++ <ε>) (⁅ i ⁆ Vec.++ preimage (λ ()) ⁅ i ⁆)    ≡⟨ merge-++ X <ε> ⁅ i ⁆ (preimage (λ ()) ⁅ i ⁆) ⟩
+        join (merge X ⁅ i ⁆) (merge <ε> (preimage (λ ()) ⁅ i ⁆)) ≡⟨ ≡.cong (join (merge X ⁅ i ⁆)) (merge-[] <ε> (preimage (λ ()) ⁅ i ⁆)) ⟩
+        join (merge X ⁅ i ⁆) U                                  ≡⟨ join-comm (merge X ⁅ i ⁆) U ⟩
+        merge X ⁅ i ⁆                                           ≡⟨ merge-⁅⁆ X i ⟩
+        X i ∎
+
+    Push-swap
+        : {n m : ℕ}
+          (X : ∣ Values n ∣)
+          (Y : ∣ Values m ∣)
+        → Push.₁ (+-swap {m}) ⟨$⟩ (X ++ Y) ≋ (Y ++ X)
+    Push-swap {n} {m} X Y i = begin
+        merge (X ++ Y) (preimage (+-swap {m}) ⁅ i ⁆)      ≡⟨ merge-preimage-ρ n+m↔m+n (X ++ Y) ⁅ i ⁆ ⟩
+        merge ((X ++ Y) ∘ +-swap {n}) ⁅ i ⁆               ≡⟨ merge-⁅⁆ ((X ++ Y) ∘ (+-swap {n})) i ⟩
+        ((X ++ Y) ∘ +-swap {n}) i                         ≡⟨ [,]-∘ (X ++ Y) (splitAt m i) ⟩
+        [ (X ++ Y) ∘ i₂ , (X ++ Y) ∘ i₁ ]′ (splitAt m i)  ≡⟨ [-,]-cong (++-↑ʳ X Y) (splitAt m i) ⟩
+        [ Y , (X ++ Y) ∘ i₁ ]′ (splitAt m i)              ≡⟨ [,-]-cong (++-↑ˡ X Y) (splitAt m i) ⟩
+        [ Y , X ]′ (splitAt m i)                          ≡⟨⟩
+        (Y ++ X) i                                        ∎
+      where
+        open ≡-Reasoning
+        open Inverse
+        module +-swap = _≅_ (+-comm {m} {n})
+        n+m↔m+n : Permutation (n + m) (m + n)
+        n+m↔m+n .to = +-swap.to
+        n+m↔m+n .from = +-swap.from
+        n+m↔m+n .to-cong ≡.refl = ≡.refl
+        n+m↔m+n .from-cong ≡.refl = ≡.refl
+        n+m↔m+n .inverse = (λ { ≡.refl → +-swap.isoˡ _ }) , (λ { ≡.refl → +-swap.isoʳ _ })
 
 open SymmetricMonoidalFunctor
 Push,++,[] : SymmetricMonoidalFunctor
@@ -331,9 +199,11 @@ Push,++,[] .isBraidedMonoidal = record
     { isMonoidal = record
         { ε = Push-ε
         ; ⊗-homo = ⊗-homomorphism
-        ; associativity = λ { {m} {n} {o} {(X , Y) , Z} i → Push-assoc X Y Z i }
-        ; unitaryˡ = λ { {n} {_ , X} i → merge-⁅⁆ X i }
-        ; unitaryʳ = λ { {n} {X , _} i → Push-unitaryʳ X i }
+        ; associativity = λ { {n} {m} {o} {(X , Y) , Z} → Push-assoc X Y Z }
+        ; unitaryˡ = λ { {n} {_ , X} → Push-unitaryˡ X }
+        ; unitaryʳ = λ { {n} {X , _} → Push-unitaryʳ X }
         }
-    ; braiding-compat = λ { {n} {m} {X , Y} i → Push-swap X Y i }
+    ; braiding-compat = λ { {n} {m} {X , Y} → Push-swap X Y }
     }
+
+module Push,++,[] = SymmetricMonoidalFunctor Push,++,[]
diff --git a/Functor/Monoidal/Instance/Nat/System.agda b/Functor/Monoidal/Instance/Nat/System.agda
index d86588f..2201c35 100644
--- a/Functor/Monoidal/Instance/Nat/System.agda
+++ b/Functor/Monoidal/Instance/Nat/System.agda
@@ -2,67 +2,79 @@
 
 module Functor.Monoidal.Instance.Nat.System where
 
-open import Function.Construct.Identity using () renaming (function to Id)
-import Function.Construct.Constant as Const
+import Categories.Category.Monoidal.Utilities as ⊗-Util
+import Data.Circuit.Value as Value
+import Data.Vec.Functional as Vec
+import Relation.Binary.PropositionalEquality as ≡
 
 open import Level using (0ℓ; suc; Level)
 
 open import Category.Monoidal.Instance.Nat using (Nat,+,0; Natop,+,0)
-open import Categories.Category.Instance.Nat using (Natop)
-open import Category.Instance.Setoids.SymmetricMonoidal {suc 0ℓ} {suc 0ℓ} using (Setoids-×)
-open import Categories.Category.Instance.SingletonSet using (SingletonSetoid)
-open import Data.Circuit.Value using (Value)
-open import Data.Setoid using (_⇒ₛ_; ∣_∣)
-open import Data.System {suc 0ℓ} using (Systemₛ; System; ≤-System)
-open import Data.System.Values Value using (Values; _≋_; module ≋)
-open import Data.Unit.Polymorphic using (⊤; tt)
-open import Data.Vec.Functional using ([])
-open import Relation.Binary using (Setoid)
-open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_)
-open import Functor.Instance.Nat.System using (Sys; map)
-open import Function.Base using (_∘_)
-open import Function.Bundles using (Func; _⟶ₛ_; _⟨$⟩_)
-open import Function.Construct.Setoid using (setoid)
 open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory; BraidedMonoidalCategory)
+open import Category.Instance.Setoids.SymmetricMonoidal {0ℓ} {0ℓ} using () renaming (Setoids-× to 0ℓ-Setoids-×)
+open import Category.Instance.Setoids.SymmetricMonoidal {suc 0ℓ} {suc 0ℓ} using (Setoids-×)
 
-open Func
-
-module _ where
-
-  open System
+module Natop,+,0 = SymmetricMonoidalCategory Natop,+,0 renaming (braidedMonoidalCategory to B)
+module 0ℓ-Setoids-× = SymmetricMonoidalCategory 0ℓ-Setoids-× renaming (braidedMonoidalCategory to B)
 
-  discrete : System 0
-  discrete .S = SingletonSetoid
-  discrete .fₛ = Const.function (Values 0) (SingletonSetoid ⇒ₛ SingletonSetoid) (Id SingletonSetoid)
-  discrete .fₒ = Const.function SingletonSetoid (Values 0) []
+open import Functor.Monoidal.Instance.Nat.Pull using (Pull,++,[])
+open import Categories.Functor.Monoidal.Braided Natop,+,0.B 0ℓ-Setoids-×.B using (module Strong)
 
-Sys-ε : SingletonSetoid {suc 0ℓ} {suc 0ℓ} ⟶ₛ Systemₛ 0
-Sys-ε = Const.function SingletonSetoid (Systemₛ 0) discrete
+Pull,++,[]B : Strong.BraidedMonoidalFunctor
+Pull,++,[]B = record { isBraidedMonoidal = Pull,++,[].isBraidedMonoidal }
+module Pull,++,[]B = Strong.BraidedMonoidalFunctor (record { isBraidedMonoidal = Pull,++,[].isBraidedMonoidal })
 
+open import Categories.Category.BinaryProducts using (module BinaryProducts)
 open import Categories.Category.Cartesian using (Cartesian)
+open import Categories.Category.Cocartesian using (Cocartesian)
+open import Categories.Category.Instance.Nat using (Nat; Nat-Cocartesian; Natop)
+open import Categories.Category.Instance.Setoids using (Setoids)
+open import Categories.Category.Instance.SingletonSet using () renaming (SingletonSetoid to ⊤ₛ)
 open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-Cartesian)
-open Cartesian (Setoids-Cartesian {suc 0ℓ} {suc 0ℓ}) using (products)
-open import Categories.Category.BinaryProducts using (module BinaryProducts)
-open BinaryProducts products using (-×-)
-open import Categories.Functor using (_∘F_)
+open import Categories.Category.Product using (Product)
 open import Categories.Category.Product using (_⁂_)
+open import Categories.Functor using (Functor)
+open import Categories.Functor using (_∘F_)
+open import Categories.Functor.Monoidal.Symmetric Nat,+,0 Setoids-× using (module Lax)
+open import Categories.NaturalTransformation.Core using (NaturalTransformation; ntHelper)
+open import Data.Circuit.Value using (Monoid)
+open import Data.Fin using (Fin)
+open import Data.Nat using (ℕ; _+_)
+open import Data.Product using (_,_; dmap; _×_) renaming (map to ×-map)
+open import Data.Product.Function.NonDependent.Setoid using (_×-function_; proj₁ₛ; proj₂ₛ; <_,_>ₛ; swapₛ)
+open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
+open import Data.Setoid using (_⇒ₛ_; ∣_∣)
+open import Data.System {suc 0ℓ} using (Systemₛ; System; discrete; _≤_)
+open import Data.System.Values Monoid using (++ₛ; splitₛ; Values; ++-cong; _++_; [])
+open import Data.System.Values Value.Monoid using (_≋_; module ≋)
+open import Data.Unit.Polymorphic using (⊤; tt)
+open import Function using (Func; _⟶ₛ_; _⟨$⟩_; _∘_; id; case_of_)
+open import Function.Construct.Constant using () renaming (function to Const)
+open import Function.Construct.Identity using () renaming (function to Id)
+open import Function.Construct.Setoid using (_∙_; setoid)
+open import Functor.Instance.Nat.Pull using (Pull)
+open import Functor.Instance.Nat.Push using (Push)
+open import Functor.Instance.Nat.System using (Sys; Sys-defs)
+open import Functor.Monoidal.Braided.Strong.Properties Pull,++,[]B using (braiding-compat-inv)
+open import Functor.Monoidal.Instance.Nat.Push using (Push,++,[])
+open import Functor.Monoidal.Strong.Properties Pull,++,[].monoidalFunctor using (associativity-inv)
+open import Functor.Monoidal.Strong.Properties Pull,++,[].monoidalFunctor using (unitaryʳ-inv; unitaryˡ-inv; module Shorthands)
+open import Relation.Binary using (Setoid)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_)
 
-open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper)
-open import Categories.Category.Cocartesian using (Cocartesian)
-open import Categories.Category.Instance.Nat using (Nat-Cocartesian)
+open module ⇒ₛ {A} {B} = Setoid (setoid {0ℓ} {0ℓ} {0ℓ} {0ℓ} A B) using (_≈_)
+
+open Cartesian (Setoids-Cartesian {suc 0ℓ} {suc 0ℓ}) using (products)
+
+open BinaryProducts products using (-×-)
 open Cocartesian Nat-Cocartesian using (module Dual; i₁; i₂; -+-; _+₁_; +-assocʳ; +-assocˡ; +-comm; +-swap; +₁∘+-swap; +₁∘i₁; +₁∘i₂)
 open Dual.op-binaryProducts using () renaming (×-assoc to +-assoc)
-open import Data.Product.Base using (_,_; dmap) renaming (map to ×-map)
+open SymmetricMonoidalCategory using () renaming (braidedMonoidalCategory to B)
 
-open import Categories.Functor using (Functor)
-open import Categories.Category.Product using (Product)
-open import Categories.Category.Instance.Nat using (Nat)
-open import Categories.Category.Instance.Setoids using (Setoids)
+open Func
 
-open import Data.Fin using (_↑ˡ_; _↑ʳ_)
-open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
-open import Data.Nat using (ℕ; _+_)
-open import Data.Product.Base using (_×_)
+Sys-ε : ⊤ₛ {suc 0ℓ} {suc 0ℓ} ⟶ₛ Systemₛ 0
+Sys-ε = Const ⊤ₛ (Systemₛ 0) (discrete 0)
 
 private
 
@@ -71,13 +83,6 @@ private
     c₁ c₂ c₃ c₄ c₅ c₆ : Level
     ℓ₁ ℓ₂ ℓ₃ ℓ₄ ℓ₅ ℓ₆ : Level
 
-open import Functor.Monoidal.Instance.Nat.Push using (++ₛ; Push,++,[]; Push-++; Push-assoc)
-open import Functor.Monoidal.Instance.Nat.Pull using (splitₛ; Pull,++,[]; ++-assoc; Pull-unitaryˡ; Pull-ε)
-open import Functor.Instance.Nat.Pull using (Pull; Pull₁; Pull-resp-≈; Pull-identity)
-open import Functor.Instance.Nat.Push using (Push₁; Push-identity)
-
-open import Data.Product.Function.NonDependent.Setoid using (_×-function_; proj₁ₛ; proj₂ₛ; <_,_>ₛ; swapₛ)
-
 _×-⇒_
     : {A : Setoid c₁ ℓ₁}
       {B : Setoid c₂ ℓ₂}
@@ -91,8 +96,6 @@ _×-⇒_
 _×-⇒_ f g .to (x , y) = to f x ×-function to g y
 _×-⇒_ f g .cong (x , y) = cong f x , cong g y
 
-open import Function.Construct.Setoid using (_∙_)
-
 ⊗ : System n × System m → System (n + m)
 ⊗ {n} {m} (S₁ , S₂) = record
     { S = S₁.S ×ₛ S₂.S
@@ -103,16 +106,6 @@ open import Function.Construct.Setoid using (_∙_)
     module S₁ = System S₁
     module S₂ = System S₂
 
-open import Category.Instance.Setoids.SymmetricMonoidal {0ℓ} {0ℓ} using () renaming (Setoids-× to 0ℓ-Setoids-×)
-module 0ℓ-Setoids-× = SymmetricMonoidalCategory 0ℓ-Setoids-× renaming (braidedMonoidalCategory to B)
-open module ⇒ₛ {A} {B} = Setoid (setoid {0ℓ} {0ℓ} {0ℓ} {0ℓ} A B) using (_≈_)
-open import Categories.Functor.Monoidal.Symmetric Natop,+,0 0ℓ-Setoids-× using (module Strong)
-open SymmetricMonoidalCategory using () renaming (braidedMonoidalCategory to B)
-module Natop,+,0 = SymmetricMonoidalCategory Natop,+,0 renaming (braidedMonoidalCategory to B)
-open import Categories.Functor.Monoidal.Braided Natop,+,0.B 0ℓ-Setoids-×.B using () renaming (module Strong to StrongB)
-open Strong using (SymmetricMonoidalFunctor)
-open StrongB using (BraidedMonoidalFunctor)
-
 opaque
 
   _~_ : {A B : Setoid 0ℓ 0ℓ} → Func A B → Func A B → Set
@@ -128,7 +121,7 @@ opaque
 
 ⊗ₛ
     : {n m : ℕ}
-    → Func (Systemₛ n ×ₛ Systemₛ m) (Systemₛ (n + m))
+    → Systemₛ n ×ₛ Systemₛ m ⟶ₛ Systemₛ (n + m)
 ⊗ₛ .to = ⊗
 ⊗ₛ {n} {m} .cong {a , b} {c , d} ((a≤c , c≤a) , (b≤d , d≤b)) = left , right
   where
@@ -136,66 +129,57 @@ opaque
     module b = System b
     module c = System c
     module d = System d
-    open ≤-System
-    module a≤c = ≤-System a≤c
-    module b≤d = ≤-System b≤d
-    module c≤a = ≤-System c≤a
-    module d≤b = ≤-System d≤b
-
-    open Setoid
-    open System
-
-    open import Data.Product.Base using (dmap)
-    open import Data.Vec.Functional.Properties using (++-cong)
-    left : ≤-System (⊗ₛ .to (a , b)) (⊗ₛ .to (c , d))
-    left = record
-        { ⇒S = a≤c.⇒S ×-function b≤d.⇒S
-        ; ≗-fₛ = λ i → dmap (a≤c.≗-fₛ (i ∘ i₁)) (b≤d.≗-fₛ (i ∘ i₂))
-        ; ≗-fₒ = λ (s₁ , s₂) → ++-cong (a.fₒ′ s₁) (c.fₒ′ (a≤c.⇒S ⟨$⟩ s₁)) (a≤c.≗-fₒ s₁) (b≤d.≗-fₒ s₂)
-        }
+    module a≤c = _≤_ a≤c
+    module b≤d = _≤_ b≤d
+    module c≤a = _≤_ c≤a
+    module d≤b = _≤_ d≤b
+
+    open _≤_
+    left : ⊗ₛ ⟨$⟩ (a , b) ≤ ⊗ₛ ⟨$⟩ (c , d)
+    left .⇒S = a≤c.⇒S ×-function b≤d.⇒S
+    left .≗-fₛ i with (i₁ , i₂) ← splitₛ ⟨$⟩ i = dmap (a≤c.≗-fₛ i₁) (b≤d.≗-fₛ i₂)
+    left .≗-fₒ = cong ++ₛ ∘ dmap a≤c.≗-fₒ b≤d.≗-fₒ
+
+    right : ⊗ₛ ⟨$⟩ (c , d) ≤ ⊗ₛ ⟨$⟩ (a , b)
+    right .⇒S = c≤a.⇒S ×-function d≤b.⇒S
+    right .≗-fₛ i with (i₁ , i₂) ← splitₛ ⟨$⟩ i = dmap (c≤a.≗-fₛ i₁) (d≤b.≗-fₛ i₂)
+    right .≗-fₒ = cong ++ₛ ∘ dmap c≤a.≗-fₒ d≤b.≗-fₒ
 
-    right : ≤-System (⊗ₛ .to (c , d)) (⊗ₛ .to (a , b))
-    right = record
-        { ⇒S = c≤a.⇒S ×-function d≤b.⇒S
-        ; ≗-fₛ = λ i → dmap (c≤a.≗-fₛ (i ∘ i₁)) (d≤b.≗-fₛ (i ∘ i₂))
-        ; ≗-fₒ = λ (s₁ , s₂) → ++-cong (c.fₒ′ s₁) (a.fₒ′ (c≤a.⇒S ⟨$⟩ s₁)) (c≤a.≗-fₒ s₁) (d≤b.≗-fₒ s₂)
-        }
+opaque
 
-open import Data.Fin using (Fin)
-
-System-⊗-≤
-    : {n n′ m m′ : ℕ}
-      (X : System n)
-      (Y : System m)
-      (f : Fin n → Fin n′)
-      (g : Fin m → Fin m′)
-    → ≤-System (⊗ (map f X , map g Y)) (map (f +₁ g) (⊗ (X , Y)))
-System-⊗-≤ {n} {n′} {m} {m′} X Y f g = record
-    { ⇒S = Id (X.S ×ₛ Y.S)
-    ; ≗-fₛ = λ i _ → cong X.fₛ (≋.sym (≡.cong i ∘ +₁∘i₁)) , cong Y.fₛ (≋.sym (≡.cong i ∘ +₁∘i₂ {f = f}))
-    ; ≗-fₒ = λ (s₁ , s₂) → Push-++ f g (X.fₒ′ s₁) (Y.fₒ′ s₂)
-    }
-  where
-    module X = System X
-    module Y = System Y
-
-System-⊗-≥
-    : {n n′ m m′ : ℕ}
-      (X : System n)
-      (Y : System m)
-      (f : Fin n → Fin n′)
-      (g : Fin m → Fin m′)
-    → ≤-System (map (f +₁ g) (⊗ (X , Y))) (⊗ (map f X , map g Y))
-System-⊗-≥ {n} {n′} {m} {m′} X Y f g = record
-    { ⇒S = Id (X.S ×ₛ Y.S)
-    -- ; ≗-fₛ = λ i _ → cong X.fₛ (≡.cong i ∘ +₁∘i₁) , cong Y.fₛ (≡.cong i ∘ +₁∘i₂ {f = f})
-    ; ≗-fₛ = λ i _ → cong (X.fₛ ×-⇒ Y.fₛ) (Pull-resp-≈ (+₁∘i₁ {n′}) {i} , Pull-resp-≈ (+₁∘i₂ {f = f}) {i})
-    ; ≗-fₒ = λ (s₁ , s₂) → ≋.sym (Push-++ f g (X.fₒ′ s₁) (Y.fₒ′ s₂))
-    }
-  where
-    module X = System X
-    module Y = System Y
-    import Relation.Binary.PropositionalEquality as ≡
+  unfolding Sys-defs
+
+  System-⊗-≤
+      : {n n′ m m′ : ℕ}
+        (X : System n)
+        (Y : System m)
+        (f : Fin n → Fin n′)
+        (g : Fin m → Fin m′)
+      → ⊗ (Sys.₁ f ⟨$⟩ X , Sys.₁ g ⟨$⟩ Y) ≤ Sys.₁ (f +₁ g) ⟨$⟩ ⊗ (X , Y)
+  System-⊗-≤ {n} {n′} {m} {m′} X Y f g = record
+      { ⇒S = Id (X.S ×ₛ Y.S)
+      ; ≗-fₛ = λ i s → cong (X.fₛ ×-⇒ Y.fₛ) (Pull,++,[].⊗-homo.⇐.sym-commute (f , g) {i}) {s}
+      ; ≗-fₒ = λ (s₁ , s₂) → Push,++,[].⊗-homo.commute (f , g) {X.fₒ′ s₁ , Y.fₒ′ s₂}
+      }
+    where
+      module X = System X
+      module Y = System Y
+
+  System-⊗-≥
+      : {n n′ m m′ : ℕ}
+        (X : System n)
+        (Y : System m)
+        (f : Fin n → Fin n′)
+        (g : Fin m → Fin m′)
+      → Sys.₁ (f +₁ g) ⟨$⟩ (⊗ (X , Y)) ≤ ⊗ (Sys.₁ f ⟨$⟩ X , Sys.₁ g ⟨$⟩ Y)
+  System-⊗-≥ {n} {n′} {m} {m′} X Y f g = record
+      { ⇒S = Id (X.S ×ₛ Y.S)
+      ; ≗-fₛ = λ i s → cong (X.fₛ ×-⇒ Y.fₛ) (Pull,++,[].⊗-homo.⇐.commute (f , g) {i}) {s}
+      ; ≗-fₒ = λ (s₁ , s₂) → Push,++,[].⊗-homo.sym-commute (f , g) {X.fₒ′ s₁ , Y.fₒ′ s₂}
+      }
+    where
+      module X = System X
+      module Y = System Y
 
 ⊗-homomorphism : NaturalTransformation (-×- ∘F (Sys ⁂ Sys)) (Sys ∘F -+-)
 ⊗-homomorphism = ntHelper record
@@ -203,220 +187,195 @@ System-⊗-≥ {n} {n′} {m} {m′} X Y f g = record
     ; commute = λ { (f , g) {X , Y} → System-⊗-≤ X Y f g , System-⊗-≥ X Y f g }
     }
 
-⊗-assoc-≤
-    : (X : System n)
-      (Y : System m)
-      (Z : System o)
-    → ≤-System (map (+-assocˡ {n}) (⊗ (⊗ (X , Y) , Z))) (⊗ (X , ⊗ (Y , Z)))
-⊗-assoc-≤ {n} {m} {o} X Y Z = record
-    { ⇒S = ×-assocˡ
-    ; ≗-fₛ = λ i ((s₁ , s₂) , s₃) → cong (X.fₛ ×-⇒ (Y.fₛ ×-⇒ Z.fₛ) ∙ assocˡ) (associativity-inv {x = i}) {s₁ , s₂ , s₃}
-    ; ≗-fₒ = λ ((s₁ , s₂) , s₃) → Push-assoc (X.fₒ′ s₁) (Y.fₒ′ s₂) (Z.fₒ′ s₃)
-    }
-  where
-    open Cartesian (Setoids-Cartesian {0ℓ} {0ℓ}) using () renaming (products to 0ℓ-products)
-    open BinaryProducts 0ℓ-products using (assocˡ)
-    open Cartesian (Setoids-Cartesian {0ℓ} {0ℓ}) using () renaming (products to prod)
-    open BinaryProducts prod using () renaming (assocˡ to ×-assocˡ)
-    module Pull,++,[] = SymmetricMonoidalFunctor Pull,++,[]
-    Pull,++,[]B : BraidedMonoidalFunctor
-    Pull,++,[]B = record { isBraidedMonoidal = Pull,++,[].isBraidedMonoidal }
-    module Pull,++,[]B = BraidedMonoidalFunctor (record { isBraidedMonoidal = Pull,++,[].isBraidedMonoidal })
-
-    open import Functor.Monoidal.Braided.Strong.Properties Pull,++,[]B using (associativity-inv)
-
-    module X = System X
-    module Y = System Y
-    module Z = System Z
-
-⊗-assoc-≥
-    : (X : System n)
-      (Y : System m)
-      (Z : System o)
-    → ≤-System (⊗ (X , ⊗ (Y , Z))) (map (+-assocˡ {n}) (⊗ (⊗ (X , Y) , Z)))
-⊗-assoc-≥ {n} {m} {o} X Y Z = record
-    { ⇒S = ×-assocʳ
-    ; ≗-fₛ = λ i (s₁ , s₂ , s₃) → cong ((X.fₛ ×-⇒ Y.fₛ) ×-⇒ Z.fₛ) (sym-split-assoc {i}) {(s₁ , s₂) , s₃}
-    ; ≗-fₒ = λ (s₁ , s₂ , s₃) → sym-++-assoc {(X.fₒ′ s₁ , Y.fₒ′ s₂) , Z.fₒ′ s₃}
-    }
-  where
-    open Cartesian (Setoids-Cartesian {0ℓ} {0ℓ}) using () renaming (products to prod)
-    open BinaryProducts prod using () renaming (assocʳ to ×-assocʳ)
-    open Cartesian (Setoids-Cartesian {0ℓ} {0ℓ}) using () renaming (products to 0ℓ-products)
-    open BinaryProducts 0ℓ-products using (×-assoc; assocˡ; assocʳ)
-
-    open import Categories.Morphism.Reasoning 0ℓ-Setoids-×.U using (switch-tofromʳ)
-    open import Categories.Functor.Monoidal.Symmetric using (module Lax)
-    module Lax₂ = Lax Nat,+,0 0ℓ-Setoids-×
-    module Pull,++,[] = Strong.SymmetricMonoidalFunctor Pull,++,[]
-    open import Functor.Monoidal.Strong.Properties Pull,++,[].monoidalFunctor using (associativity-inv)
-    module Push,++,[] = Lax₂.SymmetricMonoidalFunctor Push,++,[]
-
-    +-assocℓ : Fin ((n + m) + o) → Fin (n + (m + o))
-    +-assocℓ = +-assocˡ {n} {m} {o}
-
-    opaque
-
-      unfolding _~_
-
-      associativity-inv-~ : splitₛ ×-function Id (Values o) ∙ splitₛ ∙ Pull₁ +-assocℓ ~ assocʳ ∙ Id (Values n) ×-function splitₛ ∙ splitₛ
-      associativity-inv-~ {i} = associativity-inv {n} {m} {o} {i}
-
-      associativity-~ : Push₁ (+-assocˡ {n} {m} {o}) ∙ ++ₛ ∙ ++ₛ ×-function Id (Values o) ~ ++ₛ ∙ Id (Values n) ×-function ++ₛ ∙ assocˡ
-      associativity-~ {i} = Push,++,[].associativity {n} {m} {o} {i}
-
-    sym-split-assoc-~ : assocʳ ∙ Id (Values n) ×-function splitₛ ∙ splitₛ ~ splitₛ ×-function Id (Values o) ∙ splitₛ ∙ Pull₁ +-assocℓ
-    sym-split-assoc-~ = sym-~ associativity-inv-~
-
-    sym-++-assoc-~ : ++ₛ ∙ Id (Values n) ×-function ++ₛ ∙ assocˡ ~ Push₁ (+-assocˡ {n} {m} {o}) ∙ ++ₛ ∙ ++ₛ ×-function Id (Values o)
-    sym-++-assoc-~ = sym-~ associativity-~
-
-    opaque
-
-      unfolding _~_
-
-      sym-split-assoc : assocʳ ∙ Id (Values n) ×-function splitₛ ∙ splitₛ ≈ splitₛ ×-function Id (Values o) ∙ splitₛ ∙ Pull₁ +-assocℓ
-      sym-split-assoc {i} = sym-split-assoc-~ {i}
-
-      sym-++-assoc : ++ₛ ∙ Id (Values n) ×-function ++ₛ ∙ assocˡ ≈ Push₁ (+-assocˡ {n} {m} {o}) ∙ ++ₛ ∙ ++ₛ ×-function Id (Values o)
-      sym-++-assoc {i} = sym-++-assoc-~
-
-    module X = System X
-    module Y = System Y
-    module Z = System Z
-
-open import Function.Base using (id)
-Sys-unitaryˡ-≤  : (X : System n) → ≤-System (map id (⊗ (discrete , X))) X
-Sys-unitaryˡ-≤ X = record
-    { ⇒S = proj₂ₛ
-    ; ≗-fₛ = λ i (_ , s) → X.refl
-    ; ≗-fₒ = λ (_ , s) → Push-identity
-    }
-  where
-    module X = System X
-
-Sys-unitaryˡ-≥  : (X : System n) → ≤-System X (map id (⊗ (discrete , X)))
-Sys-unitaryˡ-≥ {n} X = record
-    { ⇒S = < Const.function X.S SingletonSetoid tt , Id X.S >ₛ
-    ; ≗-fₛ = λ i s → tt , X.refl
-    ; ≗-fₒ = λ s → Equiv.sym {x = Push₁ id} {Id (Values n)} Push-identity
-    }
-  where
-    module X = System X
-    open SymmetricMonoidalCategory 0ℓ-Setoids-× using (module Equiv)
-
-open import Data.Vec.Functional using (_++_)
+opaque
 
-Sys-unitaryʳ-≤ : (X : System n) → ≤-System (map (id ++ (λ ())) (⊗ {n} {0} (X , discrete))) X
-Sys-unitaryʳ-≤ {n} X = record
-    { ⇒S = proj₁ₛ
-    ; ≗-fₛ = λ i (s , _) → cong (X.fₛ ∙ proj₁ₛ {B = SingletonSetoid {0ℓ}}) (unitaryʳ-inv {n} {i})
-    ; ≗-fₒ = λ (s , _) → Push,++,[].unitaryʳ {n} {X.fₒ′ s , tt}
-    }
-  where
-    module X = System X
-    module Pull,++,[] = Strong.SymmetricMonoidalFunctor Pull,++,[]
-    open import Functor.Monoidal.Strong.Properties Pull,++,[].monoidalFunctor using (unitaryʳ-inv; module Shorthands)
-    open import Categories.Functor.Monoidal.Symmetric Nat,+,0 0ℓ-Setoids-× using (module Lax)
-    module Push,++,[] = Lax.SymmetricMonoidalFunctor Push,++,[]
-
-Sys-unitaryʳ-≥ : (X : System n) → ≤-System X (map (id ++ (λ ())) (⊗ {n} {0} (X , discrete)))
-Sys-unitaryʳ-≥ {n} X = record
-    { ⇒S = < Id X.S , Const.function X.S SingletonSetoid tt >ₛ
-    ; ≗-fₛ = λ i s →
-        cong
-            (X.fₛ ×-⇒ Const.function (Values 0) (SingletonSetoid ⇒ₛ SingletonSetoid) (Id (SingletonSetoid {suc 0ℓ} {0ℓ})) ∙ Id (Values n) ×-function ε⇒)
-            sym-split-unitaryʳ
-            {s , tt}
-    ; ≗-fₒ = λ s → sym-++-unitaryʳ {X.fₒ′ s , tt}
-    }
-  where
-    module X = System X
-    module Pull,++,[] = Strong.SymmetricMonoidalFunctor Pull,++,[]
-    open import Functor.Monoidal.Strong.Properties Pull,++,[].monoidalFunctor using (unitaryʳ-inv; module Shorthands)
-    open import Categories.Functor.Monoidal.Symmetric Nat,+,0 0ℓ-Setoids-× using (module Lax)
-    module Push,++,[] = Lax.SymmetricMonoidalFunctor Push,++,[]
-    import Categories.Category.Monoidal.Utilities 0ℓ-Setoids-×.monoidal as ⊗-Util
-
-    open ⊗-Util.Shorthands using (ρ⇐)
-    open Shorthands using (ε⇐; ε⇒)
-
-    sym-split-unitaryʳ
-        : ρ⇐ ≈ Id (Values n) ×-function ε⇐ ∙ splitₛ ∙ Pull₁ (id ++ (λ ()))
-    sym-split-unitaryʳ =
-        0ℓ-Setoids-×.Equiv.sym
-            {Values n}
-            {Values n ×ₛ SingletonSetoid}
-            {Id (Values n) ×-function ε⇐ ∙ splitₛ ∙ Pull₁ (id ++ (λ ()))}
-            {ρ⇐}
-            (unitaryʳ-inv {n})
-
-    sym-++-unitaryʳ : proj₁ₛ {B = SingletonSetoid {0ℓ} {0ℓ}} ≈ Push₁ (id ++ (λ ())) ∙ ++ₛ ∙ Id (Values n) ×-function ε⇒
-    sym-++-unitaryʳ =
-        0ℓ-Setoids-×.Equiv.sym
-            {Values n ×ₛ SingletonSetoid}
-            {Values n}
-            {Push₁ (id ++ (λ ())) ∙ ++ₛ ∙ Id (Values n) ×-function ε⇒}
-            {proj₁ₛ}
-            (Push,++,[].unitaryʳ {n})
-
-Sys-braiding-compat-≤
-    : (X : System n)
-      (Y : System m)
-    → ≤-System (map (+-swap {m} {n}) (⊗ (X , Y))) (⊗ (Y , X))
-Sys-braiding-compat-≤ {n} {m} X Y = record
-    { ⇒S = swapₛ
-    ; ≗-fₛ = λ i (s₁ , s₂) → cong (Y.fₛ ×-⇒ X.fₛ ∙ swapₛ) (braiding-compat-inv {m} {n} {i}) {s₂ , s₁}
-    ; ≗-fₒ = λ (s₁ , s₂) → Push,++,[].braiding-compat {n} {m} {X.fₒ′ s₁ , Y.fₒ′ s₂}
-    }
-  where
-    module X = System X
-    module Y = System Y
-    module Pull,++,[] = SymmetricMonoidalFunctor Pull,++,[]
-    Pull,++,[]B : BraidedMonoidalFunctor
-    Pull,++,[]B = record { isBraidedMonoidal = Pull,++,[].isBraidedMonoidal }
-    open import Functor.Monoidal.Braided.Strong.Properties Pull,++,[]B using (braiding-compat-inv)
-    open import Categories.Functor.Monoidal.Symmetric Nat,+,0 0ℓ-Setoids-× using (module Lax)
-    module Push,++,[] = Lax.SymmetricMonoidalFunctor Push,++,[]
-
-Sys-braiding-compat-≥
-    : (X : System n)
-      (Y : System m)
-    → ≤-System (⊗ (Y , X)) (map (+-swap {m} {n}) (⊗ (X , Y)))
-Sys-braiding-compat-≥ {n} {m} X Y = record
-    { ⇒S = swapₛ
-    ; ≗-fₛ = λ i (s₂ , s₁) → cong (X.fₛ ×-⇒ Y.fₛ) (sym-braiding-compat-inv {i})
-    ; ≗-fₒ = λ (s₂ , s₁) → sym-braiding-compat-++ {X.fₒ′ s₁ , Y.fₒ′ s₂}
-    }
-  where
-    module X = System X
-    module Y = System Y
-    module Pull,++,[] = SymmetricMonoidalFunctor Pull,++,[]
-    Pull,++,[]B : BraidedMonoidalFunctor
-    Pull,++,[]B = record { isBraidedMonoidal = Pull,++,[].isBraidedMonoidal }
-    open import Functor.Monoidal.Braided.Strong.Properties Pull,++,[]B using (braiding-compat-inv)
-    open import Categories.Functor.Monoidal.Symmetric Nat,+,0 0ℓ-Setoids-× using (module Lax)
-    module Push,++,[] = Lax.SymmetricMonoidalFunctor Push,++,[]
-
-    sym-braiding-compat-inv : swapₛ ∙ splitₛ {m} ≈ splitₛ ∙ Pull₁ (+-swap {m} {n})
-    sym-braiding-compat-inv {i} =
-        0ℓ-Setoids-×.Equiv.sym
-            {Values (m + n)}
-            {Values n ×ₛ Values m}
-            {splitₛ ∙ Pull₁ (+-swap {m} {n})}
-            {swapₛ ∙ splitₛ {m}}
-            (λ {j} → braiding-compat-inv {m} {n} {j}) {i}
-
-    sym-braiding-compat-++ : ++ₛ {m} ∙ swapₛ ≈ Push₁ (+-swap {m} {n}) ∙ ++ₛ
-    sym-braiding-compat-++ {i} =
-        0ℓ-Setoids-×.Equiv.sym
-            {Values n ×ₛ Values m}
-            {Values (m + n)}
-            {Push₁ (+-swap {m} {n}) ∙ ++ₛ}
-            {++ₛ {m} ∙ swapₛ}
-            (Push,++,[].braiding-compat {n} {m})
+  unfolding Sys-defs
+
+  ⊗-assoc-≤
+      : (X : System n)
+        (Y : System m)
+        (Z : System o)
+      → Sys.₁ (+-assocˡ {n}) ⟨$⟩ (⊗ (⊗ (X , Y) , Z)) ≤ ⊗ (X , ⊗ (Y , Z))
+  ⊗-assoc-≤ {n} {m} {o} X Y Z = record
+      { ⇒S = assocˡ
+      ; ≗-fₛ = λ i ((s₁ , s₂) , s₃) → cong (X.fₛ ×-⇒ (Y.fₛ ×-⇒ Z.fₛ) ∙ assocˡ) (associativity-inv {x = i}) {s₁ , s₂ , s₃}
+      ; ≗-fₒ = λ ((s₁ , s₂) , s₃) → Push,++,[].associativity {x = (X.fₒ′ s₁ , Y.fₒ′ s₂) , Z.fₒ′ s₃}
+      }
+    where
+      open Cartesian (Setoids-Cartesian {0ℓ} {0ℓ}) using () renaming (products to 0ℓ-products)
+      open BinaryProducts 0ℓ-products using (assocˡ)
+
+      module X = System X
+      module Y = System Y
+      module Z = System Z
+
+  ⊗-assoc-≥
+      : (X : System n)
+        (Y : System m)
+        (Z : System o)
+      → ⊗ (X , ⊗ (Y , Z)) ≤ Sys.₁ (+-assocˡ {n}) ⟨$⟩ (⊗ (⊗ (X , Y) , Z))
+  ⊗-assoc-≥ {n} {m} {o} X Y Z = record
+      { ⇒S = ×-assocʳ
+      ; ≗-fₛ = λ i (s₁ , s₂ , s₃) → cong ((X.fₛ ×-⇒ Y.fₛ) ×-⇒ Z.fₛ) (sym-split-assoc {i}) {(s₁ , s₂) , s₃}
+      ; ≗-fₒ = λ (s₁ , s₂ , s₃) → sym-++-assoc {(X.fₒ′ s₁ , Y.fₒ′ s₂) , Z.fₒ′ s₃}
+      }
+    where
+      open Cartesian (Setoids-Cartesian {0ℓ} {0ℓ}) using () renaming (products to prod)
+      open BinaryProducts prod using () renaming (assocʳ to ×-assocʳ; assocˡ to ×-assocˡ)
+
+      +-assocℓ : Fin ((n + m) + o) → Fin (n + (m + o))
+      +-assocℓ = +-assocˡ {n} {m} {o}
+
+      opaque
+
+        unfolding _~_
+
+        associativity-inv-~ : splitₛ ×-function Id (Values o) ∙ splitₛ ∙ Pull.₁ +-assocℓ ~ ×-assocʳ ∙ Id (Values n) ×-function splitₛ ∙ splitₛ
+        associativity-inv-~ {i} = associativity-inv {n} {m} {o} {i}
+
+        associativity-~ : Push.₁ (+-assocˡ {n} {m} {o}) ∙ ++ₛ ∙ ++ₛ ×-function Id (Values o) ~ ++ₛ ∙ Id (Values n) ×-function ++ₛ ∙ ×-assocˡ
+        associativity-~ {i} = Push,++,[].associativity {n} {m} {o} {i}
+
+      sym-split-assoc-~ : ×-assocʳ ∙ Id (Values n) ×-function splitₛ ∙ splitₛ ~ splitₛ ×-function Id (Values o) ∙ splitₛ ∙ Pull.₁ +-assocℓ
+      sym-split-assoc-~ = sym-~ associativity-inv-~
+
+      sym-++-assoc-~ : ++ₛ ∙ Id (Values n) ×-function ++ₛ ∙ ×-assocˡ ~ Push.₁ (+-assocˡ {n} {m} {o}) ∙ ++ₛ ∙ ++ₛ ×-function Id (Values o)
+      sym-++-assoc-~ = sym-~ associativity-~
+
+      opaque
+
+        unfolding _~_
+
+        sym-split-assoc : ×-assocʳ ∙ Id (Values n) ×-function splitₛ ∙ splitₛ ≈ splitₛ ×-function Id (Values o) ∙ splitₛ ∙ Pull.₁ +-assocℓ
+        sym-split-assoc {i} = sym-split-assoc-~ {i}
+
+        sym-++-assoc : ++ₛ ∙ Id (Values n) ×-function ++ₛ ∙ ×-assocˡ ≈ Push.₁ (+-assocˡ {n} {m} {o}) ∙ ++ₛ ∙ ++ₛ ×-function Id (Values o)
+        sym-++-assoc {i} = sym-++-assoc-~
+
+      module X = System X
+      module Y = System Y
+      module Z = System Z
+
+  Sys-unitaryˡ-≤  : (X : System n) → Sys.₁ id ⟨$⟩ (⊗ (discrete 0 , X)) ≤ X
+  Sys-unitaryˡ-≤ {n} X = record
+      { ⇒S = proj₂ₛ
+      ; ≗-fₛ = λ i (_ , s) → cong (X.fₛ ∙ proj₂ₛ {A = ⊤ₛ {0ℓ}}) (unitaryˡ-inv {n} {i})
+      ; ≗-fₒ = λ (_ , s) → Push,++,[].unitaryˡ {n} {tt , X.fₒ′ s}
+      }
+    where
+      module X = System X
+
+  Sys-unitaryˡ-≥  : (X : System n) → X ≤ Sys.₁ id ⟨$⟩ (⊗ (discrete 0 , X))
+  Sys-unitaryˡ-≥ {n} X = record
+      { ⇒S = < Const X.S ⊤ₛ tt , Id X.S >ₛ
+      ; ≗-fₛ = λ i s → cong (disc.fₛ ×-⇒ X.fₛ ∙ ε⇒ ×-function Id (Values n)) (sym-split-unitaryˡ {i})
+      ; ≗-fₒ = λ s → sym-++-unitaryˡ {_ , X.fₒ′ s}
+      }
+    where
+      module X = System X
+      open SymmetricMonoidalCategory 0ℓ-Setoids-× using (module Equiv)
+      open ⊗-Util.Shorthands 0ℓ-Setoids-×.monoidal using (λ⇐)
+      open Shorthands using (ε⇐; ε⇒)
+      module disc = System (discrete 0)
+      sym-split-unitaryˡ
+          : λ⇐ ≈ ε⇐ ×-function Id (Values n) ∙ splitₛ ∙ Pull.₁ ((λ ()) Vec.++ id)
+      sym-split-unitaryˡ =
+          0ℓ-Setoids-×.Equiv.sym
+              {Values n}
+              {⊤ₛ ×ₛ Values n}
+              {ε⇐ ×-function Id (Values n) ∙ splitₛ ∙ Pull.₁ ((λ ()) Vec.++ id)}
+              {λ⇐}
+              (unitaryˡ-inv {n})
+      sym-++-unitaryˡ : proj₂ₛ {A = ⊤ₛ {0ℓ} {0ℓ}} ≈ Push.₁ ((λ ()) Vec.++ id) ∙ ++ₛ ∙ Push,++,[].ε ×-function Id (Values n)
+      sym-++-unitaryˡ =
+          0ℓ-Setoids-×.Equiv.sym
+              {⊤ₛ ×ₛ Values n}
+              {Values n}
+              {Push.₁ ((λ ()) Vec.++ id) ∙ ++ₛ ∙ Push,++,[].ε ×-function Id (Values n)}
+              {proj₂ₛ}
+              (Push,++,[].unitaryˡ {n})
+
+
+  Sys-unitaryʳ-≤ : (X : System n) → Sys.₁ (id Vec.++ (λ ())) ⟨$⟩ (⊗ {n} {0} (X , discrete 0)) ≤ X
+  Sys-unitaryʳ-≤ {n} X = record
+      { ⇒S = proj₁ₛ
+      ; ≗-fₛ = λ i (s , _) → cong (X.fₛ ∙ proj₁ₛ {B = ⊤ₛ {0ℓ}}) (unitaryʳ-inv {n} {i})
+      ; ≗-fₒ = λ (s , _) → Push,++,[].unitaryʳ {n} {X.fₒ′ s , tt}
+      }
+    where
+      module X = System X
+
+  Sys-unitaryʳ-≥ : (X : System n) → X ≤ Sys.₁ (id Vec.++ (λ ())) ⟨$⟩ (⊗ {n} {0} (X , discrete 0))
+  Sys-unitaryʳ-≥ {n} X = record
+      { ⇒S = < Id X.S , Const X.S ⊤ₛ tt >ₛ
+      ; ≗-fₛ = λ i s → cong (X.fₛ ×-⇒ disc.fₛ ∙ Id (Values n) ×-function ε⇒) sym-split-unitaryʳ {s , tt}
+      ; ≗-fₒ = λ s → sym-++-unitaryʳ {X.fₒ′ s , tt}
+      }
+    where
+      module X = System X
+      module disc = System (discrete 0)
+      open ⊗-Util.Shorthands 0ℓ-Setoids-×.monoidal using (ρ⇐)
+      open Shorthands using (ε⇐; ε⇒)
+      sym-split-unitaryʳ
+          : ρ⇐ ≈ Id (Values n) ×-function ε⇐ ∙ splitₛ ∙ Pull.₁ (id Vec.++ (λ ()))
+      sym-split-unitaryʳ =
+          0ℓ-Setoids-×.Equiv.sym
+              {Values n}
+              {Values n ×ₛ ⊤ₛ}
+              {Id (Values n) ×-function ε⇐ ∙ splitₛ ∙ Pull.₁ (id Vec.++ (λ ()))}
+              {ρ⇐}
+              (unitaryʳ-inv {n})
+      sym-++-unitaryʳ : proj₁ₛ {B = ⊤ₛ {0ℓ}} ≈ Push.₁ (id Vec.++ (λ ())) ∙ ++ₛ ∙ Id (Values n) ×-function Push,++,[].ε
+      sym-++-unitaryʳ =
+          0ℓ-Setoids-×.Equiv.sym
+              {Values n ×ₛ ⊤ₛ}
+              {Values n}
+              {Push.₁ (id Vec.++ (λ ())) ∙ ++ₛ ∙ Id (Values n) ×-function Push,++,[].ε}
+              {proj₁ₛ}
+              (Push,++,[].unitaryʳ {n})
+
+  Sys-braiding-compat-≤
+      : (X : System n)
+        (Y : System m)
+      → Sys.₁ (+-swap {m} {n}) ⟨$⟩ (⊗ (X , Y)) ≤ ⊗ (Y , X)
+  Sys-braiding-compat-≤ {n} {m} X Y = record
+      { ⇒S = swapₛ
+      ; ≗-fₛ = λ i (s₁ , s₂) → cong (Y.fₛ ×-⇒ X.fₛ ∙ swapₛ) (braiding-compat-inv {m} {n} {i}) {s₂ , s₁}
+      ; ≗-fₒ = λ (s₁ , s₂) → Push,++,[].braiding-compat {n} {m} {X.fₒ′ s₁ , Y.fₒ′ s₂}
+      }
+    where
+      module X = System X
+      module Y = System Y
+
+  Sys-braiding-compat-≥
+      : (X : System n)
+        (Y : System m)
+      → ⊗ (Y , X) ≤ Sys.₁ (+-swap {m} {n}) ⟨$⟩ ⊗ (X , Y)
+  Sys-braiding-compat-≥ {n} {m} X Y = record
+      { ⇒S = swapₛ
+      ; ≗-fₛ = λ i (s₂ , s₁) → cong (X.fₛ ×-⇒ Y.fₛ) (sym-braiding-compat-inv {i})
+      ; ≗-fₒ = λ (s₂ , s₁) → sym-braiding-compat-++ {X.fₒ′ s₁ , Y.fₒ′ s₂}
+      }
+    where
+      module X = System X
+      module Y = System Y
+      sym-braiding-compat-inv : swapₛ ∙ splitₛ {m} ≈ splitₛ ∙ Pull.₁ (+-swap {m} {n})
+      sym-braiding-compat-inv {i} =
+          0ℓ-Setoids-×.Equiv.sym
+              {Values (m + n)}
+              {Values n ×ₛ Values m}
+              {splitₛ ∙ Pull.₁ (+-swap {m} {n})}
+              {swapₛ ∙ splitₛ {m}}
+              (λ {j} → braiding-compat-inv {m} {n} {j}) {i}
+      sym-braiding-compat-++ : ++ₛ {m} ∙ swapₛ ≈ Push.₁ (+-swap {m} {n}) ∙ ++ₛ
+      sym-braiding-compat-++ {i} =
+          0ℓ-Setoids-×.Equiv.sym
+              {Values n ×ₛ Values m}
+              {Values (m + n)}
+              {Push.₁ (+-swap {m} {n}) ∙ ++ₛ}
+              {++ₛ {m} ∙ swapₛ}
+              (Push,++,[].braiding-compat {n} {m})
 
-open import Categories.Functor.Monoidal.Symmetric Nat,+,0 Setoids-× using (module Lax)
 open Lax.SymmetricMonoidalFunctor
 
 Sys,⊗,ε : Lax.SymmetricMonoidalFunctor
@@ -431,3 +390,5 @@ Sys,⊗,ε .isBraidedMonoidal = record
         }
     ; braiding-compat = λ { {n} {m} {X , Y} → Sys-braiding-compat-≤ X Y , Sys-braiding-compat-≥ X Y }
     }
+
+module Sys,⊗,ε = Lax.SymmetricMonoidalFunctor Sys,⊗,ε
author	Jacques Comeaux <jacquesrcomeaux@protonmail.com>	2025-11-09 17:12:29 -0600
committer	Jacques Comeaux <jacquesrcomeaux@protonmail.com>	2025-11-09 17:12:29 -0600
commit	6a5154cf29d98ab644b5def52c55f213d1076e2b (patch)
tree	2a6ddd6034607f36f4441fe3d1bd6e71e4264cb3
parent	b2b2bdaa75406451174f0873cfd355e7511abd9a (diff)