4 files changed, 1124 insertions, 0 deletions
diff --git a/Functor/Monoidal/Instance/Nat/Preimage.agda b/Functor/Monoidal/Instance/Nat/Preimage.agda
new file mode 100644
index 0000000..59c9391
--- /dev/null
+++ b/Functor/Monoidal/Instance/Nat/Preimage.agda
@@ -0,0 +1,164 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Functor.Monoidal.Instance.Nat.Preimage where
+
+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.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.Product using (_⁂_)
+open import Categories.Functor using (_∘F_)
+open import Data.Subset.Functional using (Subset)
+open import Data.Nat.Base using (ℕ; _+_)
+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.Preimage using (Preimage; Subsetₛ)
+open import Level using (0ℓ)
+
+open Cartesian (Setoids-Cartesian {0ℓ} {0ℓ}) using (products)
+open BinaryProducts products using (-×-)
+open Cocartesian Nat-Cocartesian using (module Dual; _+₁_; +-assocʳ; +-swap; +₁∘+-swap)
+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.Properties using (splitAt-join; splitAt-↑ˡ)
+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 Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_; module ≡-Reasoning)
+open import Data.Bool.Base using (Bool)
+
+open Func
+Preimage-ε : SingletonSetoid {0ℓ} {0ℓ} ⟶ₛ Subsetₛ 0
+to Preimage-ε x = []
+cong Preimage-ε x ()
+
+++ₛ : {n m : ℕ} → Subsetₛ n ×ₛ Subsetₛ m ⟶ₛ Subsetₛ (n + m)
+to ++ₛ (xs , ys) = xs ++ ys
+cong ++ₛ (≗xs , ≗ys) = ++-cong _ _ ≗xs ≗ys
+
+preimage-++
+    : {n n′ m m′ : ℕ}
+      (f : Fin n → Fin n′)
+      (g : Fin m → Fin m′)
+      {xs : Subset n′}
+      {ys : Subset m′}
+    → preimage f xs ++ preimage g ys ≗ preimage (f +₁ g) (xs ++ ys)
+preimage-++ {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 : NaturalTransformation (-×- ∘F (Preimage ⁂ Preimage)) (Preimage ∘F -+-)
+⊗-homomorphism = ntHelper record
+    { η = λ (n , m) → ++ₛ {n} {m}
+    ; commute = λ { {n′ , m′} {n , m} (f , g) {xs , ys} e → preimage-++ f g e }
+    }
+
+open import Category.Instance.Setoids.SymmetricMonoidal {0ℓ} {0ℓ} using (Setoids-×)
+open import Categories.Functor.Monoidal.Symmetric Natop,+,0 Setoids-× using (module Lax)
+open Lax using (SymmetricMonoidalFunctor)
+
+++-assoc
+    : {m n o : ℕ}
+      (X : Subset m)
+      (Y : Subset n)
+      (Z : Subset 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 ]′ ∘ splitAt m , Z ]′ (splitAt (m + n) (+-assocʳ {m} i))          ≡⟨ [,]-cong ([,]-cong (inv ∘ X) (inv ∘ Y) ∘ splitAt m) (inv ∘ Z) (splitAt (m + n) (+-assocʳ {m} i)) ⟨
+    [ [ b ∘ X′ , b ∘ Y′ ]′ ∘ splitAt m , b ∘ Z′ ]′ (splitAt _ (+-assocʳ {m} i)) ≡⟨ [-,]-cong ([,]-∘ b ∘ splitAt m) (splitAt (m + n) (+-assocʳ {m} i)) ⟨
+    [ b ∘ [ X′ , Y′ ]′ ∘ splitAt m , b ∘ Z′ ]′ (splitAt _ (+-assocʳ {m} i))     ≡⟨ [,]-∘ b (splitAt (m + n) (+-assocʳ {m} i)) ⟨
+    b ([ [ X′ , Y′ ]′ ∘ splitAt m , Z′ ]′ (splitAt _ (+-assocʳ {m} i)))         ≡⟨ ≡.cong b ([]∘assocʳ {2} {m} i) ⟩
+    b ([ X′ , [ Y′ , Z′ ]′ ∘ splitAt n ]′ (splitAt m i))                        ≡⟨ [,]-∘ b (splitAt m i) ⟩
+    [ b ∘ X′ , b ∘ [ Y′ , Z′ ]′ ∘ splitAt n ]′ (splitAt m i)                    ≡⟨ [,-]-cong ([,]-∘ b ∘ splitAt n) (splitAt m i) ⟩
+    [ b ∘ X′ , [ b ∘ Y′ , b ∘ Z′ ]′ ∘ splitAt n ]′ (splitAt m i)                ≡⟨ [,]-cong (inv ∘ X) ([,]-cong (inv ∘ Y) (inv ∘ Z) ∘ splitAt n) (splitAt m i) ⟩
+    [ X , [ Y , Z ]′ ∘ splitAt n ]′ (splitAt m i)                               ≡⟨⟩
+    (X ++ (Y ++ Z)) i                                                           ∎
+  where
+    open Bool
+    open Fin
+    f : Bool → Fin 2
+    f false = zero
+    f true = suc zero
+    b : Fin 2 → Bool
+    b zero = false
+    b (suc zero) = true
+    inv : b ∘ f ≗ id
+    inv false = ≡.refl
+    inv true = ≡.refl
+    X′ : Fin m → Fin 2
+    X′ = f ∘ X
+    Y′ : Fin n → Fin 2
+    Y′ = f ∘ Y
+    Z′ : Fin o → Fin 2
+    Z′ = f ∘ Z
+    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
+
+++-swap
+    : {n m : ℕ}
+      (X : Subset n)
+      (Y : Subset m)
+    → (X ++ Y) ∘ +-swap {n} ≗ Y ++ X
+++-swap {n} {m} X Y i = begin
+    [ X , Y ]′ (splitAt n (+-swap {n} i))           ≡⟨ [,]-cong (inv ∘ X) (inv ∘ Y) (splitAt n (+-swap {n} i)) ⟨
+    [ b ∘ X′ , b ∘ Y′ ]′ (splitAt n (+-swap {n} i)) ≡⟨ [,]-∘ b (splitAt n (+-swap {n} i)) ⟨
+    b ([ X′ , Y′ ]′ (splitAt n (+-swap {n} i)))     ≡⟨ ≡.cong b ([]∘swap {2} {n} i) ⟩
+    b ([ Y′ , X′ ]′ (splitAt m i))                  ≡⟨ [,]-∘ b (splitAt m i) ⟩
+    [ b ∘ Y′ , b ∘ X′ ]′ (splitAt m i)              ≡⟨ [,]-cong (inv ∘ Y) (inv ∘ X) (splitAt m i) ⟩
+    [ Y  , X ]′ (splitAt m i)                       ∎
+  where
+    open Bool
+    open Fin
+    f : Bool → Fin 2
+    f false = zero
+    f true = suc zero
+    b : Fin 2 → Bool
+    b zero = false
+    b (suc zero) = true
+    inv : b ∘ f ≗ id
+    inv false = ≡.refl
+    inv true = ≡.refl
+    X′ : Fin n → Fin 2
+    X′ = f ∘ X
+    Y′ : Fin m → Fin 2
+    Y′ = f ∘ Y
+    open ≡-Reasoning
+
+open SymmetricMonoidalFunctor
+Preimage,++,[] : SymmetricMonoidalFunctor
+Preimage,++,[] .F = Preimage
+Preimage,++,[] .isBraidedMonoidal = record
+    { isMonoidal = record
+        { ε = Preimage-ε
+        ; ⊗-homo = ⊗-homomorphism
+        ; associativity = λ { {m} {n} {o} {(X , Y) , Z} i → ++-assoc X Y Z i }
+        ; unitaryˡ = λ _ → ≡.refl
+        ; unitaryʳ = λ { {n} {X , _} i → Preimage-unitaryˡ X i }
+        }
+    ; braiding-compat = λ { {n} {m} {X , Y} i → ++-swap X Y i }
+    }
diff --git a/Functor/Monoidal/Instance/Nat/Pull.agda b/Functor/Monoidal/Instance/Nat/Pull.agda
new file mode 100644
index 0000000..c2b6958
--- /dev/null
+++ b/Functor/Monoidal/Instance/Nat/Pull.agda
@@ -0,0 +1,192 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Functor.Monoidal.Instance.Nat.Pull where
+
+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.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 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.Properties using (splitAt-join; splitAt-↑ˡ; splitAt-↑ʳ; join-splitAt)
+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 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 Func
+
+module _ where
+
+  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
+  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ʳ _ })
+
+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 }
+        }
+    ; braiding-compat = λ { {n} {m} {X , Y} i → Pull-swap X Y i }
+    }
diff --git a/Functor/Monoidal/Instance/Nat/Push.agda b/Functor/Monoidal/Instance/Nat/Push.agda
new file mode 100644
index 0000000..30ed745
--- /dev/null
+++ b/Functor/Monoidal/Instance/Nat/Push.agda
@@ -0,0 +1,339 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Functor.Monoidal.Instance.Nat.Push where
+
+open import Categories.Category.Instance.Nat using (Nat)
+open import Data.Bool.Base using (Bool; false)
+open import Data.Subset.Functional using (Subset; ⁅_⁆; ⊥)
+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 Categories.NaturalTransformation using (NaturalTransformation; ntHelper)
+open import Data.Vec.Functional using (Vector; []; _++_; head; tail)
+open import Data.Vec.Functional.Properties using (++-cong)
+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 Cartesian (Setoids-Cartesian {0ℓ} {0ℓ}) using (products)
+open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory)
+open import Categories.Category.Instance.Nat using (Nat-Cocartesian)
+open import Categories.Category.Cocartesian using (Cocartesian; module BinaryCoproducts)
+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.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.Fin.Base using (splitAt; _↑ˡ_; _↑ʳ_) renaming (join to joinAt)
+open import Data.Fin.Properties using (splitAt-↑ˡ; splitAt-↑ʳ; splitAt⁻¹-↑ˡ; splitAt⁻¹-↑ʳ; ↑ˡ-injective; ↑ʳ-injective; _≟_; 2↔Bool)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≢_; _≗_; module ≡-Reasoning)
+open BinaryProducts products using (-×-)
+open Value using (U)
+open Bool using (false)
+
+open import Function.Bundles using (Equivalence)
+open import Category.Monoidal.Instance.Nat using (Nat,+,0)
+open import Category.Instance.Setoids.SymmetricMonoidal {0ℓ} {0ℓ} using (Setoids-×)
+open import Categories.Functor.Monoidal.Symmetric Nat,+,0 Setoids-× using (module Lax)
+open Lax using (SymmetricMonoidalFunctor)
+open import Categories.Morphism Nat using (_≅_)
+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 ℕ
+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 ℕ
+
+    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                     ∎
+      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                       ∎
+      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 SymmetricMonoidalFunctor
+Push,++,[] : SymmetricMonoidalFunctor
+Push,++,[] .F = Push
+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 }
+        }
+    ; braiding-compat = λ { {n} {m} {X , Y} i → Push-swap X Y i }
+    }
diff --git a/Functor/Monoidal/Instance/Nat/System.agda b/Functor/Monoidal/Instance/Nat/System.agda
new file mode 100644
index 0000000..1b3bb34
--- /dev/null
+++ b/Functor/Monoidal/Instance/Nat/System.agda
@@ -0,0 +1,429 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level; 0ℓ; suc)
+
+module Functor.Monoidal.Instance.Nat.System {ℓ : Level} where
+
+open import Function.Construct.Identity using () renaming (function to Id)
+import Function.Construct.Constant as Const
+
+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 ℓ} {ℓ} 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 {ℓ} 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 Func
+
+module _ where
+
+  open System
+
+  discrete : System 0
+  discrete .S = SingletonSetoid
+  discrete .fₛ = Const.function (Values 0) (SingletonSetoid ⇒ₛ SingletonSetoid) (Id SingletonSetoid)
+  discrete .fₒ = Const.function SingletonSetoid (Values 0) []
+
+Sys-ε : SingletonSetoid {suc ℓ} {ℓ} ⟶ₛ Systemₛ 0
+Sys-ε = Const.function SingletonSetoid (Systemₛ 0) discrete
+
+open import Categories.Category.Cartesian using (Cartesian)
+open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-Cartesian)
+open Cartesian (Setoids-Cartesian {suc ℓ} {ℓ}) 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 (_⁂_)
+
+open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper)
+open import Categories.Category.Cocartesian using (Cocartesian)
+open import Categories.Category.Instance.Nat using (Nat-Cocartesian)
+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 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 import Data.Fin using (_↑ˡ_; _↑ʳ_)
+open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
+open import Data.Nat using (ℕ; _+_)
+open import Data.Product.Base using (_×_)
+
+private
+
+  variable
+    n m o : ℕ
+    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₂ ℓ₂}
+      {C : Setoid c₃ ℓ₃}
+      {D : Setoid c₄ ℓ₄}
+      {E : Setoid c₅ ℓ₅}
+      {F : Setoid c₆ ℓ₆}
+    → A ⟶ₛ B ⇒ₛ C
+    → D ⟶ₛ E ⇒ₛ F
+    → A ×ₛ D ⟶ₛ B ×ₛ E ⇒ₛ C ×ₛ F
+_×-⇒_ 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
+    ; fₛ = S₁.fₛ ×-⇒ S₂.fₛ ∙ splitₛ
+    ; fₒ = ++ₛ ∙ S₁.fₒ ×-function S₂.fₒ
+    }
+  where
+    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
+  _~_ = _≈_
+  infix 4 _~_
+
+  sym-~
+      : {A B : Setoid 0ℓ 0ℓ}
+        {x y : Func A B}
+      → x ~ y
+      → y ~ x
+  sym-~ {A} {B} {x} {y} = 0ℓ-Setoids-×.Equiv.sym {A} {B} {x} {y}
+
+⊗ₛ
+    : {n m : ℕ}
+    → Func (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
+    module a = System a
+    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₂)
+        }
+
+    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₂)
+        }
+
+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 ≡
+
+⊗-homomorphism : NaturalTransformation (-×- ∘F (Sys ⁂ Sys)) (Sys ∘F -+-)
+⊗-homomorphism = ntHelper record
+    { η = λ (n , m) → ⊗ₛ {n} {m}
+    ; 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 {ℓ} {ℓ}) using () renaming (products to prod)
+    open BinaryProducts prod using () renaming (assocˡ to ×-assocˡ)
+    module Pull,++,[] = SymmetricMonoidalFunctor Pull,++,[]
+    module Pull,++,[]B = BraidedMonoidalFunctor (record { isBraidedMonoidal = Pull,++,[].isBraidedMonoidal })
+
+    open import Functor.Monoidal.Braided.Strong.Properties Pull,++,[].braidedMonoidalFunctor 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 {ℓ} {ℓ}) 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 (_++_)
+
+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 {ℓ} {ℓ})) ∙ 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,++,[]
+    module Pull,++,[]B = BraidedMonoidalFunctor (record { isBraidedMonoidal = Pull,++,[].isBraidedMonoidal })
+    open import Functor.Monoidal.Braided.Strong.Properties Pull,++,[].braidedMonoidalFunctor 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,++,[]
+    module Pull,++,[]B = BraidedMonoidalFunctor (record { isBraidedMonoidal = Pull,++,[].isBraidedMonoidal })
+    open import Functor.Monoidal.Braided.Strong.Properties Pull,++,[].braidedMonoidalFunctor 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})
+
+open import Categories.Functor.Monoidal.Symmetric Nat,+,0 Setoids-× using (module Lax)
+open Lax.SymmetricMonoidalFunctor
+
+Sys,⊗,ε : Lax.SymmetricMonoidalFunctor
+Sys,⊗,ε .F = Sys
+Sys,⊗,ε .isBraidedMonoidal = record
+    { isMonoidal = record
+        { ε = Sys-ε
+        ; ⊗-homo = ⊗-homomorphism
+        ; associativity = λ { {n} {m} {o} {(X , Y), Z} → ⊗-assoc-≤ X Y Z , ⊗-assoc-≥ X Y Z }
+        ; unitaryˡ = λ { {n} {_ , X} → Sys-unitaryˡ-≤ X , Sys-unitaryˡ-≥ X }
+        ; unitaryʳ = λ { {n} {X , _} → Sys-unitaryʳ-≤ X , Sys-unitaryʳ-≥ X }
+        }
+    ; braiding-compat = λ { {n} {m} {X , Y} → Sys-braiding-compat-≤ X Y , Sys-braiding-compat-≥ X Y }
+    }