Clean up System functors

1 files changed, 295 insertions, 334 deletions

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,⊗,ε