Define Sys functor from Nat to SMCs

4 files changed, 547 insertions, 75 deletions

diff --git a/Data/Setoid.agda b/Data/Setoid.agda
index 454d276..8a9929a 100644
--- a/Data/Setoid.agda
+++ b/Data/Setoid.agda
@@ -2,7 +2,49 @@
 
 module Data.Setoid where
 
-open import Relation.Binary using (Setoid)
+open import Data.Product using (_,_)
+open import Data.Product.Function.NonDependent.Setoid using (_×-function_)
+open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
+open import Function using (Func; _⟶ₛ_)
 open import Function.Construct.Setoid using () renaming (setoid to infixr 0 _⇒ₛ_) public
+open import Level using (Level)
+open import Relation.Binary using (Setoid)
 
 open Setoid renaming (Carrier to ∣_∣) public
+
+open Func
+
+_×-⇒_
+    : {c₁ c₂ c₃ c₄ c₅ c₆ : Level}
+      {ℓ₁ ℓ₂ ℓ₃ ℓ₄ ℓ₅ ℓ₆ : Level}
+      {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
+
+assocₛ⇒
+    : {c₁ c₂ c₃ : Level}
+      {ℓ₁ ℓ₂ ℓ₃ : Level}
+      {A : Setoid c₁ ℓ₁}
+      {B : Setoid c₂ ℓ₂}
+      {C : Setoid c₃ ℓ₃}
+    → (A ×ₛ B) ×ₛ C ⟶ₛ A ×ₛ (B ×ₛ C)
+assocₛ⇒ .to ((x , y) , z) = x , (y , z)
+assocₛ⇒ .cong ((≈x , ≈y) , ≈z) = ≈x , (≈y , ≈z)
+
+assocₛ⇐
+    : {c₁ c₂ c₃ : Level}
+      {ℓ₁ ℓ₂ ℓ₃ : Level}
+      {A : Setoid c₁ ℓ₁}
+      {B : Setoid c₂ ℓ₂}
+      {C : Setoid c₃ ℓ₃}
+    → A ×ₛ (B ×ₛ C) ⟶ₛ (A ×ₛ B) ×ₛ C
+assocₛ⇐ .to (x , (y , z)) = (x , y) , z
+assocₛ⇐ .cong (≈x , (≈y , ≈z)) = (≈x , ≈y) , ≈z
diff --git a/Data/System/Monoidal.agda b/Data/System/Monoidal.agda
new file mode 100644
index 0000000..f4f5311
--- /dev/null
+++ b/Data/System/Monoidal.agda
@@ -0,0 +1,187 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Data.Nat using (ℕ)
+open import Level using (Level; suc; 0ℓ)
+
+module Data.System.Monoidal {ℓ : Level} (n : ℕ) where
+
+open import Data.System {ℓ} using (System; Systems; _≤_; ≤-refl; ≤-trans; _≈_; discrete)
+
+open import Categories.Category.Monoidal using (Monoidal)
+open import Categories.Category.Monoidal.Symmetric using (Symmetric)
+open import Categories.Category.Monoidal.Bundle using (MonoidalCategory; SymmetricMonoidalCategory)
+open import Categories.Functor using (Functor)
+open import Categories.Functor.Bifunctor using (Bifunctor; flip-bifunctor)
+open import Categories.Morphism (Systems n) using (_≅_; Iso)
+open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; niHelper)
+open import Data.Circuit.Value using (Monoid)
+open import Data.Product using (_,_; _×_; uncurry′)
+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 (_⇒ₛ_; _×-⇒_; assocₛ⇒; assocₛ⇐)
+open import Data.System.Values Monoid using (Values; _⊕_; ⊕-cong; ⊕-identityˡ; ⊕-identityʳ; ⊕-assoc; ⊕-comm; module ≋)
+open import Function using (Func; _⟶ₛ_)
+open import Function.Construct.Setoid using (_∙_)
+open import Relation.Binary using (Setoid)
+
+open _≤_
+open Setoid
+
+module _ where
+
+  open Func
+
+  δₛ : Values n ⟶ₛ Values n ×ₛ Values n
+  δₛ .to v = v , v
+  δₛ .cong v≋w = v≋w , v≋w
+
+  ⊕ₛ : Values n ×ₛ Values n ⟶ₛ Values n
+  ⊕ₛ .to (v , w) = v ⊕ w
+  ⊕ₛ .cong (v₁≋v₂ , w₁≋w₂) = ⊕-cong v₁≋v₂ w₁≋w₂
+
+_⊗₀_ : System n → System n → System n
+_⊗₀_ X Y = let open System in record
+    { S = S X ×ₛ S Y
+    ; fₛ = fₛ X ×-⇒ fₛ Y ∙ δₛ
+    ; fₒ = ⊕ₛ ∙ fₒ X ×-function fₒ Y
+    }
+
+_⊗₁_
+    : {A A′ B B′ : System n}
+      (f : A ≤ A′)
+      (g : B ≤ B′)
+    → A ⊗₀ B ≤ A′ ⊗₀ B′
+_⊗₁_ f g .⇒S = ⇒S f ×-function ⇒S g
+_⊗₁_ f g .≗-fₛ i (s₁ , s₂) = ≗-fₛ f i s₁ , ≗-fₛ g i s₂
+_⊗₁_ f g .≗-fₒ (s₁ , s₂) = ⊕-cong (≗-fₒ f s₁) (≗-fₒ g s₂)
+
+module _ where
+
+  open Functor
+  open System
+
+  ⊗ : Bifunctor (Systems n) (Systems n) (Systems n)
+  ⊗ .F₀ = uncurry′ _⊗₀_
+  ⊗ .F₁ = uncurry′ _⊗₁_
+  ⊗ .identity {X , Y} = refl (S X) , refl (S Y)
+  ⊗ .homomorphism {_} {_} {X″ , Y″} = refl (S X″) , refl (S Y″)
+  ⊗ .F-resp-≈ (f≈f′ , g≈g′) = f≈f′ , g≈g′
+
+module Unitors {X : System n} where
+
+  open System X
+
+  ⊗-discreteˡ-≤ : discrete n ⊗₀ X ≤ X
+  ⊗-discreteˡ-≤ .⇒S = proj₂ₛ
+  ⊗-discreteˡ-≤ .≗-fₛ i s = S.refl
+  ⊗-discreteˡ-≤ .≗-fₒ (_ , s) = ⊕-identityˡ (fₒ′ s)
+
+  ⊗-discreteˡ-≥ : X ≤ discrete n ⊗₀ X
+  ⊗-discreteˡ-≥ .⇒S = record { to = λ s → _ , s ; cong = λ s≈s′ → _ , s≈s′ }
+  ⊗-discreteˡ-≥ .≗-fₛ i s = _ , S.refl
+  ⊗-discreteˡ-≥ .≗-fₒ s = ≋.sym (⊕-identityˡ (fₒ′ s))
+
+  ⊗-discreteʳ-≤ : X ⊗₀ discrete n ≤ X
+  ⊗-discreteʳ-≤ .⇒S = proj₁ₛ
+  ⊗-discreteʳ-≤ .≗-fₛ i s = S.refl
+  ⊗-discreteʳ-≤ .≗-fₒ (s , _) = ⊕-identityʳ (fₒ′ s)
+
+  ⊗-discreteʳ-≥ : X ≤ X ⊗₀ discrete n
+  ⊗-discreteʳ-≥ .⇒S = record { to = λ s → s , _ ; cong = λ s≈s′ → s≈s′ , _ }
+  ⊗-discreteʳ-≥ .≗-fₛ i s = S.refl , _
+  ⊗-discreteʳ-≥ .≗-fₒ s = ≋.sym (⊕-identityʳ (fₒ′ s))
+
+  open _≅_
+  open Iso
+
+  unitorˡ : discrete n ⊗₀ X ≅ X
+  unitorˡ .from = ⊗-discreteˡ-≤
+  unitorˡ .to = ⊗-discreteˡ-≥
+  unitorˡ .iso .isoˡ = _ , S.refl
+  unitorˡ .iso .isoʳ = S.refl
+
+  unitorʳ : X ⊗₀ discrete n ≅ X
+  unitorʳ .from = ⊗-discreteʳ-≤
+  unitorʳ .to = ⊗-discreteʳ-≥
+  unitorʳ .iso .isoˡ = S.refl , _
+  unitorʳ .iso .isoʳ = S.refl
+
+open Unitors using (unitorˡ; unitorʳ) public
+
+module Associator {X Y Z : System n} where
+
+  module X = System X
+  module Y = System Y
+  module Z = System Z
+
+  assoc-≤ : (X ⊗₀ Y) ⊗₀ Z ≤ X ⊗₀ (Y ⊗₀ Z)
+  assoc-≤ .⇒S = assocₛ⇒
+  assoc-≤ .≗-fₛ i ((s₁ , s₂) , s₃) = X.S.refl , Y.S.refl , Z.S.refl
+  assoc-≤ .≗-fₒ ((s₁ , s₂) , s₃) = ⊕-assoc (X.fₒ′ s₁) (Y.fₒ′ s₂) (Z.fₒ′ s₃)
+
+  assoc-≥ : X ⊗₀ (Y ⊗₀ Z) ≤ (X ⊗₀ Y) ⊗₀ Z
+  assoc-≥ .⇒S = assocₛ⇐
+  assoc-≥ .≗-fₛ i (s₁ , (s₂ , s₃)) = (X.S.refl , Y.S.refl) , Z.S.refl
+  assoc-≥ .≗-fₒ (s₁ , (s₂ , s₃)) = ≋.sym (⊕-assoc (X.fₒ′ s₁) (Y.fₒ′ s₂) (Z.fₒ′ s₃) )
+
+  open _≅_
+  open Iso
+
+  associator : (X ⊗₀ Y) ⊗₀ Z ≅ X ⊗₀ (Y ⊗₀ Z)
+  associator .from = assoc-≤
+  associator .to = assoc-≥
+  associator .iso .isoˡ = (X.S.refl , Y.S.refl) , Z.S.refl
+  associator .iso .isoʳ = X.S.refl , Y.S.refl , Z.S.refl
+
+open Associator using (associator) public
+
+Systems-Monoidal : Monoidal (Systems n)
+Systems-Monoidal = let open System in record
+    { ⊗ = ⊗
+    ; unit = discrete n
+    ; unitorˡ = unitorˡ
+    ; unitorʳ = unitorʳ
+    ; associator = associator
+    ; unitorˡ-commute-from = λ {_} {Y} → refl (S Y)
+    ; unitorˡ-commute-to = λ {_} {Y} → _ , refl (S Y)
+    ; unitorʳ-commute-from = λ {_} {Y} → refl (S Y)
+    ; unitorʳ-commute-to = λ {_} {Y} → refl (S Y) , _
+    ; assoc-commute-from = λ {_} {X′} {_} {_} {Y′} {_} {_} {Z′} → refl (S X′) , refl (S Y′) , refl (S Z′)
+    ; assoc-commute-to = λ {_} {X′} {_} {_} {Y′} {_} {_} {Z′} → (refl (S X′) , refl (S Y′)) , refl (S Z′)
+    ; triangle = λ {X} {Y} → refl (S X) , refl (S Y)
+    ; pentagon = λ {W} {X} {Y} {Z} → refl (S W) , refl (S X) , refl (S Y) , refl (S Z)
+    }
+
+open System
+
+⊗-swap-≤ : {X Y : System n} → Y ⊗₀ X ≤ X ⊗₀ Y
+⊗-swap-≤ .⇒S = swapₛ
+⊗-swap-≤ {X} {Y} .≗-fₛ i (s₁ , s₂) = refl (S X) , refl (S Y)
+⊗-swap-≤ {X} {Y} .≗-fₒ (s₁ , s₂) = ⊕-comm (fₒ′ Y s₁) (fₒ′ X s₂)
+
+braiding : ⊗ ≃ flip-bifunctor ⊗
+braiding = niHelper record
+    { η = λ (X , Y) → ⊗-swap-≤
+    ; η⁻¹ = λ (X , Y) → ⊗-swap-≤
+    ; commute = λ { {X , Y} {X′ , Y′} (f , g) → refl (S Y′) , refl (S X′) }
+    ; iso = λ (X , Y) → record
+        { isoˡ = refl (S X) , refl (S Y)
+        ; isoʳ = refl (S Y) , refl (S X)
+        }
+    }
+
+Systems-Symmetric : Symmetric Systems-Monoidal
+Systems-Symmetric = record
+    { braided = record
+        { braiding = braiding
+        ; hexagon₁ = λ {X} {Y} {Z} → refl (S Y) , refl (S Z) , refl (S X)
+        ; hexagon₂ = λ {X} {Y} {Z} → (refl (S Z) , refl (S X)) , refl (S Y)
+        }
+    ; commutative = λ {X} {Y} → refl (S Y) , refl (S X)
+    }
+
+Systems-MC : MonoidalCategory (suc 0ℓ) ℓ 0ℓ
+Systems-MC = record { monoidal = Systems-Monoidal }
+
+Systems-SMC : SymmetricMonoidalCategory (suc 0ℓ) ℓ 0ℓ
+Systems-SMC = record { symmetric = Systems-Symmetric }
diff --git a/Functor/Instance/Nat/Push.agda b/Functor/Instance/Nat/Push.agda
index 71b9a63..c417ebf 100644
--- a/Functor/Instance/Nat/Push.agda
+++ b/Functor/Instance/Nat/Push.agda
@@ -15,7 +15,7 @@ open import Data.Fin.Preimage using (preimage; preimage-cong₁)
 open import Data.Nat using (ℕ)
 open import Data.Setoid using (∣_∣; _⇒ₛ_)
 open import Data.Subset.Functional using (⁅_⁆)
-open import Data.System.Values Monoid using (Values; module Object; _⊕_; <ε>; _≋_; ≋-isEquiv; merge; push; merge-⊕; merge-<ε>; merge-cong; merge-⁅⁆; merge-push; merge-cong₂)
+open import Data.System.Values Monoid using (Values; module Object; _⊕_; <ε>; _≋_; ≋-isEquiv; merge; push; merge-⊕; merge-<ε>; merge-cong; merge-⁅⁆; merge-push; merge-cong₂; lookup)
 open import Function using (Func; _⟶ₛ_; _⟨$⟩_; _∘_; id)
 open import Function.Construct.Identity using () renaming (function to Id)
 open import Function.Construct.Setoid using (_∙_)
@@ -31,79 +31,79 @@ private
 
   variable A B C : ℕ
 
-  -- Push sends a natural number n to Values n
-  Push₀ : ℕ → CommutativeMonoid
-  Push₀ n = Valuesₘ n
+-- Push sends a natural number n to Values n
+Push₀ : ℕ → CommutativeMonoid
+Push₀ n = Valuesₘ n
 
-  -- action of Push on morphisms (covariant)
+-- action of Push on morphisms (covariant)
 
-  opaque
+opaque
 
-    unfolding Values
+  unfolding Values
 
-    open CommutativeMonoid using (Carrier)
-    open CommutativeMonoid⇒ using (arr)
+  open CommutativeMonoid using (Carrier)
+  open CommutativeMonoid⇒ using (arr)
 
-    -- setoid morphism
-    Pushₛ : (Fin A → Fin B) → Values A ⟶ₛ Values B
-    Pushₛ f .to v = merge v ∘ preimage f ∘ ⁅_⁆
-    Pushₛ f .cong x≗y i = merge-cong (preimage f ⁅ i ⁆) x≗y
+  -- setoid morphism
+  Pushₛ : (Fin A → Fin B) → Values A ⟶ₛ Values B
+  Pushₛ f .to v = merge v ∘ preimage f ∘ ⁅_⁆
+  Pushₛ f .cong x≗y i = merge-cong (preimage f ⁅ i ⁆) x≗y
 
-  opaque
+private opaque
 
-    unfolding Pushₛ _⊕_
+  unfolding Pushₛ _⊕_
 
-    Push-⊕
-        : (f : Fin A → Fin B)
-        → (xs ys : ∣ Values A ∣)
-        → Pushₛ f ⟨$⟩ (xs ⊕ ys)
-        ≋ (Pushₛ f ⟨$⟩ xs) ⊕ (Pushₛ f ⟨$⟩ ys)
-    Push-⊕ f xs ys i = merge-⊕ xs ys (preimage f ⁅ i ⁆)
+  Push-⊕
+      : (f : Fin A → Fin B)
+      → (xs ys : ∣ Values A ∣)
+      → Pushₛ f ⟨$⟩ (xs ⊕ ys)
+      ≋ (Pushₛ f ⟨$⟩ xs) ⊕ (Pushₛ f ⟨$⟩ ys)
+  Push-⊕ f xs ys i = merge-⊕ xs ys (preimage f ⁅ i ⁆)
 
-    Push-<ε>
-        : (f : Fin A → Fin B)
-        → Pushₛ f ⟨$⟩ <ε> ≋ <ε>
-    Push-<ε> f i = merge-<ε> (preimage f ⁅ i ⁆)
+  Push-<ε>
+      : (f : Fin A → Fin B)
+      → Pushₛ f ⟨$⟩ <ε> ≋ <ε>
+  Push-<ε> f i = merge-<ε> (preimage f ⁅ i ⁆)
 
-  opaque
+opaque
 
-    unfolding Push-⊕ ≋-isEquiv Valuesₘ
+  unfolding Valuesₘ ≋-isEquiv
 
-    -- monoid morphism
-    Pushₘ : (Fin A → Fin B) → CommutativeMonoid⇒ (Valuesₘ A) (Valuesₘ B)
-    Pushₘ f = record
-        { monoid⇒ = record
-            { arr = Pushₛ f
-            ; preserves-μ = Push-⊕ f _ _
-            ; preserves-η = Push-<ε> f
-            }
-        }
+  -- monoid morphism
+  Pushₘ : (Fin A → Fin B) → CommutativeMonoid⇒ (Valuesₘ A) (Valuesₘ B)
+  Pushₘ f = record
+      { monoid⇒ = record
+          { arr = Pushₛ f
+          ; preserves-μ = Push-⊕ f _ _
+          ; preserves-η = Push-<ε> f
+          }
+      }
 
-    -- Push respects identity
-    Push-identity
-      : (open Setoid (Carrier (Push₀ A) ⇒ₛ Carrier (Push₀ A)))
-      → arr (Pushₘ id) ≈ Id (Carrier (Push₀ A))
-    Push-identity {_} {v} i = merge-⁅⁆ v i
+private opaque
 
-  opaque
+  unfolding Pushₘ Pushₛ push lookup
 
-    unfolding Pushₘ push
+  -- Push respects identity
+  Push-identity
+    : (open Setoid (Carrier (Push₀ A) ⇒ₛ Carrier (Push₀ A)))
+    → arr (Pushₘ id) ≈ Id (Carrier (Push₀ A))
+  Push-identity {_} {v} i = merge-⁅⁆ v i
 
-    -- Push respects composition
-    Push-homomorphism
-        : {f : Fin A → Fin B}
-          {g : Fin B → Fin C}
-        → (open Setoid (Carrier (Push₀ A) ⇒ₛ Carrier (Push₀ C)))
-        → arr (Pushₘ (g ∘ f)) ≈ arr (Pushₘ g) ∙ arr (Pushₘ f)
-    Push-homomorphism {f = f} {g} {v} = merge-push f g v
+  -- Push respects composition
+  Push-homomorphism
+      : {f : Fin A → Fin B}
+        {g : Fin B → Fin C}
+      → (open Setoid (Carrier (Push₀ A) ⇒ₛ Carrier (Push₀ C)))
+      → arr (Pushₘ (g ∘ f)) ≈ arr (Pushₘ g) ∙ arr (Pushₘ f)
+  Push-homomorphism {f = f} {g} {v} = merge-push f g v
 
-    -- Push respects equality
-    Push-resp-≈
-        : {f g : Fin A → Fin B}
-        → f ≗ g
-        → (open Setoid (Carrier (Push₀ A) ⇒ₛ Carrier (Push₀ B)))
-        → arr (Pushₘ f) ≈ arr (Pushₘ g)
-    Push-resp-≈ f≗g {v} = merge-cong₂ v ∘ preimage-cong₁ f≗g ∘ ⁅_⁆
+  -- Push respects equality
+  Push-resp-≈
+      : {f g : Fin A → Fin B}
+      → f ≗ g
+      → (open Setoid (Carrier (Push₀ A) ⇒ₛ Carrier (Push₀ B)))
+      → arr (Pushₘ f) ≈ arr (Pushₘ g)
+  Push-resp-≈ f≗g {v} = merge-cong₂ v ∘ preimage-cong₁ f≗g ∘ ⁅_⁆
 
 -- the Push functor
 Push : Functor Nat CMonoids
diff --git a/Functor/Instance/Nat/System.agda b/Functor/Instance/Nat/System.agda
index 4a651f2..728fec8 100644
--- a/Functor/Instance/Nat/System.agda
+++ b/Functor/Instance/Nat/System.agda
@@ -1,38 +1,61 @@
 {-# OPTIONS --without-K --safe #-}
 {-# OPTIONS --hidden-argument-puns #-}
+{-# OPTIONS --lossy-unification #-}
 
 module Functor.Instance.Nat.System where
 
 open import Level using (suc; 0ℓ)
 
-open import Categories.Category.Instance.Nat using (Nat)
+import Data.System.Monoidal {suc 0ℓ} as System-⊗
+import Categories.Morphism as Morphism
+import Functor.Free.Instance.SymmetricMonoidalPreorder.Strong as SymmetricMonoidalPreorder
+
+open import Category.Instance.Setoids.SymmetricMonoidal using (Setoids-×)
+
 open import Categories.Category using (Category)
 open import Categories.Category.Instance.Cats using (Cats)
-open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; niHelper)
+open import Categories.Category.Instance.Monoidals using (StrongMonoidals)
+open import Categories.Category.Instance.Nat using (Nat)
+open import Categories.Category.Monoidal.Bundle using (MonoidalCategory; SymmetricMonoidalCategory)
+open import Categories.Category.Product using (_⁂_)
 open import Categories.Functor using (Functor; _∘F_) renaming (id to idF)
+open import Categories.Functor.Monoidal using (StrongMonoidalFunctor)
+open import Categories.Functor.Monoidal.Properties using (idF-StrongMonoidal; ∘-StrongMonoidal)
+open import Categories.Functor.Monoidal.Symmetric using () renaming (module Strong to Strong₃)
+open import Categories.Functor.Monoidal.Symmetric.Properties using (idF-StrongSymmetricMonoidal; ∘-StrongSymmetricMonoidal)
+open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; niHelper; NaturalIsomorphism)
+open import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal using () renaming (module Strong to Strong₂)
+open import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal.Symmetric using () renaming (module Strong to Strong₄)
+open import Category.Construction.CMonoids (Setoids-×.symmetric {suc 0ℓ} {suc 0ℓ}) using (CMonoids)
+open import Category.Instance.SymMonCat using () renaming (module Strong to Strong₁)
 open import Data.Circuit.Value using (Monoid)
 open import Data.Fin using (Fin)
 open import Data.Nat using (ℕ)
-open import Data.Product.Base using (_,_; _×_)
+open import Data.Product using (_,_; _×_)
+open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
 open import Data.Setoid using (∣_∣)
-open import Data.System {suc 0ℓ} using (System; _≤_; Systemₛ; Systems; ≤-refl; ≤-trans; _≈_)
+open import Data.Setoid.Unit using (⊤ₛ)
+open import Data.System {suc 0ℓ} using (System; _≤_; Systemₛ; Systems; ≤-refl; ≤-trans; _≈_; discrete)
+open import Data.System.Monoidal {suc 0ℓ} using (Systems-MC; Systems-SMC)
 open import Data.System.Values Monoid using (module ≋; module Object; Values; ≋-isEquiv)
-open import Relation.Binary using (Setoid)
 open import Function using (Func; _⟶ₛ_; _⟨$⟩_; _∘_; id)
 open import Function.Construct.Identity using () renaming (function to Id)
 open import Function.Construct.Setoid using (_∙_)
+open import Functor.Free.Instance.InducedCMonoid using (InducedCMonoid)
 open import Functor.Instance.Nat.Pull using (Pull)
 open import Functor.Instance.Nat.Push using (Push)
+open import Object.Monoid.Commutative (Setoids-×.symmetric {0ℓ} {0ℓ}) using (CommutativeMonoid; CommutativeMonoid⇒)
+open import Relation.Binary using (Setoid)
 open import Relation.Binary.PropositionalEquality as ≡ using (_≗_)
 
-open import Category.Instance.Setoids.SymmetricMonoidal {0ℓ} {0ℓ} using (Setoids-×)
-open import Category.Construction.CMonoids Setoids-×.symmetric using (CMonoids)
-open import Object.Monoid.Commutative Setoids-×.symmetric using (CommutativeMonoid; CommutativeMonoid⇒)
-
 open CommutativeMonoid⇒ using (arr)
-open Object using (Valuesₘ)
 open Func
 open Functor
+open Object using (Valuesₘ)
+open Strong₁ using (SymMonCat)
+open Strong₂ using (MonoidalNaturalIsomorphism)
+open Strong₃ using (SymmetricMonoidalFunctor)
+open Strong₄ using (SymmetricMonoidalNaturalIsomorphism)
 open _≤_
 
 private
@@ -250,11 +273,231 @@ Sys-resp-≈ f≗g = niHelper record
         }
     }
 
-Sys : Functor Nat (Cats (suc 0ℓ) (suc 0ℓ) 0ℓ)
-Sys .F₀ = Systems
-Sys .F₁ = Sys₁
-Sys .identity = Sys-identity
-Sys .homomorphism = Sys-homo _ _
-Sys .F-resp-≈ = Sys-resp-≈
+module NatCat where
+
+  Sys : Functor Nat (Cats (suc 0ℓ) (suc 0ℓ) 0ℓ)
+  Sys .F₀ = Systems
+  Sys .F₁ = Sys₁
+  Sys .identity = Sys-identity
+  Sys .homomorphism = Sys-homo _ _
+  Sys .F-resp-≈ = Sys-resp-≈
+
+  module Sys = Functor Sys
+
+module NatMC where
+
+  module _ (f : Fin A → Fin B) where
+
+    module A = System-⊗ A
+    module B = System-⊗ B
+
+    open CommutativeMonoid⇒ (Push.₁ f)
+    open Morphism (Systems B) using (_≅_)
+
+    opaque
+      unfolding map
+      ε-≅ : discrete B ≅ map f (discrete A)
+      ε-≅ = record
+          -- other fields can be inferred
+          { from = record
+              { ⇒S = Id ⊤ₛ
+              ; ≗-fₒ = λ s → ≋.sym preserves-η
+              }
+          ; to = record
+              { ⇒S = Id ⊤ₛ
+              ; ≗-fₒ = λ s → preserves-η
+              }
+          }
+
+    opaque
+      unfolding map-≤
+      ⊗-homo-≃ : B.⊗ ∘F (Sys₁ f ⁂ Sys₁ f) ≃ Sys₁ f ∘F A.⊗
+      ⊗-homo-≃ = niHelper record
+          { η = λ (X , Y) → record
+              { ⇒S = Id (S X ×ₛ S Y)
+              ; ≗-fₛ = λ i s → Setoid.refl (S X ×ₛ S Y)
+              ; ≗-fₒ = λ (s₁ , s₂) → ≋.sym preserves-μ
+              }
+          ; η⁻¹ = λ (X , Y) → record
+              { ⇒S = Id (S X ×ₛ S Y)
+              ; ≗-fₛ = λ i s → Setoid.refl (S X ×ₛ S Y)
+              ; ≗-fₒ = λ s → preserves-μ
+              }
+          ; commute = λ { {_} {Z′ , Y′} _ → Setoid.refl (S Z′ ×ₛ S Y′) }
+          ; iso = λ (X , Y) → record
+              { isoˡ = Setoid.refl (S X ×ₛ S Y)
+              ; isoʳ = Setoid.refl (S X ×ₛ S Y)
+              }
+          }
+
+    private
+
+      module ε-≅ = _≅_ ε-≅
+      module ⊗-homo-≃ = NaturalIsomorphism ⊗-homo-≃
+      module A-MC = MonoidalCategory A.Systems-MC
+      module B-MC = MonoidalCategory B.Systems-MC
+
+      F : Functor (Systems A) (Systems B)
+      F = Sys₁ f
+
+      module F = Functor F
+
+    open B-MC using () renaming (_∘_ to _∘′_)
+
+    opaque
+
+      unfolding ⊗-homo-≃
+
+      associativity
+          : {X Y Z : System A}
+          → F.₁ A.Associator.assoc-≤
+          ∘′ ⊗-homo-≃.⇒.η (X A.⊗₀ Y , Z)
+          ∘′ ⊗-homo-≃.⇒.η (X , Y) B.⊗₁ B-MC.id
+          B-MC.≈ ⊗-homo-≃.⇒.η (X , Y A.⊗₀ Z)
+          ∘′ B-MC.id B.⊗₁ ⊗-homo-≃.⇒.η (Y , Z) 
+          ∘′ B.Associator.assoc-≤
+      associativity {X} {Y} {Z} = Setoid.refl (S X ×ₛ (S Y ×ₛ S Z))
+
+      unitaryˡ
+          : {X : System A}
+          →  F.₁ A.Unitors.⊗-discreteˡ-≤
+          ∘′ ⊗-homo-≃.⇒.η (A-MC.unit , X)
+          ∘′ ε-≅.from B.⊗₁ B-MC.id 
+          B-MC.≈ B-MC.unitorˡ.from
+      unitaryˡ {X} = Setoid.refl (S X)
+
+      unitaryʳ
+          : {X : System A}
+          →  F.₁ A.Unitors.⊗-discreteʳ-≤
+          ∘′ ⊗-homo-≃.⇒.η (X , discrete A)
+          ∘′ B-MC.id B.⊗₁ ε-≅.from
+          B-MC.≈ B-MC.unitorʳ.from
+      unitaryʳ {X} = Setoid.refl (S X)
+
+    Sys-MC₁ : StrongMonoidalFunctor (Systems-MC A) (Systems-MC B)
+    Sys-MC₁ = record
+        { F = Sys₁ f
+        ; isStrongMonoidal = record
+            { ε = ε-≅
+            ; ⊗-homo = ⊗-homo-≃
+            ; associativity = associativity
+            ; unitaryˡ = unitaryˡ
+            ; unitaryʳ = unitaryʳ
+            }
+        }
+
+  opaque
+    unfolding map-id-≤ ⊗-homo-≃
+    Sys-MC-identity : MonoidalNaturalIsomorphism (Sys-MC₁ id) (idF-StrongMonoidal (Systems-MC A))
+    Sys-MC-identity = record
+        { U = NatCat.Sys.identity
+        ; F⇒G-isMonoidal = record
+            { ε-compat = _
+            ; ⊗-homo-compat = λ {X Y} → Setoid.refl (S X ×ₛ S Y)
+            }
+        }
+
+  opaque
+    unfolding map-∘-≤ ⊗-homo-≃
+    Sys-MC-homomorphism
+        : {g : Fin B → Fin C}
+          {f : Fin A → Fin B}
+        → MonoidalNaturalIsomorphism (Sys-MC₁ (g ∘ f)) (∘-StrongMonoidal (Sys-MC₁ g) (Sys-MC₁ f))
+    Sys-MC-homomorphism = record
+        { U = NatCat.Sys.homomorphism
+        ; F⇒G-isMonoidal = record
+            { ε-compat = _
+            ; ⊗-homo-compat = λ {X Y} → Setoid.refl (S X ×ₛ S Y)
+            }
+        }
+
+  opaque
+    unfolding map-cong-≤ ⊗-homo-≃
+    Sys-MC-resp-≈
+        : {f g : Fin A → Fin B}
+        → f ≗ g
+        → MonoidalNaturalIsomorphism (Sys-MC₁ f) (Sys-MC₁ g)
+    Sys-MC-resp-≈ f≗g = record
+        { U = NatCat.Sys.F-resp-≈ f≗g
+        ; F⇒G-isMonoidal = record
+            { ε-compat = _
+            ; ⊗-homo-compat = λ {X Y} → Setoid.refl (S X ×ₛ S Y)
+            }
+        }
+
+  Sys : Functor Nat (StrongMonoidals (suc 0ℓ) (suc 0ℓ) 0ℓ)
+  Sys .F₀ = Systems-MC
+  Sys .F₁ = Sys-MC₁
+  Sys .identity = Sys-MC-identity
+  Sys .homomorphism = Sys-MC-homomorphism
+  Sys .F-resp-≈ = Sys-MC-resp-≈
+
+  module Sys = Functor Sys
+
+module NatSMC where
+
+  module _ (f : Fin A → Fin B) where
+
+    private
+
+      module A = System-⊗ A
+      module B = System-⊗ B
+      module A-SMC = SymmetricMonoidalCategory A.Systems-SMC
+      module B-SMC = SymmetricMonoidalCategory B.Systems-SMC
+
+      F : Functor (Systems A) (Systems B)
+      F = Sys₁ f
+
+      module F = Functor F
+
+      F-MF : StrongMonoidalFunctor (Systems-MC A) (Systems-MC B)
+      F-MF = NatMC.Sys.₁ f
+      module F-MF = StrongMonoidalFunctor F-MF
+
+    opaque
+      unfolding NatMC.⊗-homo-≃
+      σ-compat
+          : {X Y : System A}
+          → F.₁ (A-SMC.braiding.⇒.η (X , Y)) B-SMC.∘ F-MF.⊗-homo.⇒.η (X , Y)
+          B-SMC.≈ F-MF.⊗-homo.⇒.η (Y , X) B-SMC.∘ B-SMC.braiding.⇒.η (F.₀ X , F.₀ Y)
+      σ-compat {X} {Y} = Setoid.refl (S Y ×ₛ S X)
+
+    Sys-SMC₁ : SymmetricMonoidalFunctor (Systems-SMC A) (Systems-SMC B)
+    Sys-SMC₁ = record
+        { F-MF
+        ; isBraidedMonoidal = record
+            { F-MF
+            ; braiding-compat = σ-compat
+            }
+        }
+
+  Sys-SMC-identity : SymmetricMonoidalNaturalIsomorphism (Sys-SMC₁ id) (idF-StrongSymmetricMonoidal (Systems-SMC A))
+  Sys-SMC-identity = record { MonoidalNaturalIsomorphism NatMC.Sys.identity }
+
+  Sys-SMC-homomorphism
+      : {g : Fin B → Fin C}
+        {f : Fin A → Fin B}
+      → SymmetricMonoidalNaturalIsomorphism (Sys-SMC₁ (g ∘ f)) (∘-StrongSymmetricMonoidal (Sys-SMC₁ g) (Sys-SMC₁ f))
+  Sys-SMC-homomorphism = record { MonoidalNaturalIsomorphism NatMC.Sys.homomorphism }
+
+  Sys-SMC-resp-≈
+      : {f g : Fin A → Fin B}
+      → f ≗ g
+      → SymmetricMonoidalNaturalIsomorphism (Sys-SMC₁ f) (Sys-SMC₁ g)
+  Sys-SMC-resp-≈ f≗g = record { MonoidalNaturalIsomorphism (NatMC.Sys.F-resp-≈ f≗g) }
+
+  Sys : Functor Nat (SymMonCat {suc 0ℓ} {suc 0ℓ} {0ℓ})
+  Sys .F₀ = Systems-SMC
+  Sys .F₁ = Sys-SMC₁
+  Sys .identity = Sys-SMC-identity
+  Sys .homomorphism = Sys-SMC-homomorphism
+  Sys .F-resp-≈ = Sys-SMC-resp-≈
+
+  module Sys = Functor Sys
+
+module NatCMon where
+
+  Sys : Functor Nat CMonoids
+  Sys = InducedCMonoid ∘F SymmetricMonoidalPreorder.Free ∘F NatSMC.Sys
 
-module Sys = Functor Sys
+  module Sys = Functor Sys