Generalize systems to (co)commutative (co)monoids

2 files changed, 304 insertions, 48 deletions

diff --git a/Functor/Instance/Nat/System.agda b/Functor/Instance/Nat/System.agda
index 34ae65a..b9b89e4 100644
--- a/Functor/Instance/Nat/System.agda
+++ b/Functor/Instance/Nat/System.agda
@@ -6,7 +6,7 @@ module Functor.Instance.Nat.System where
 
 open import Level using (suc; 0ℓ)
 
-import Data.System.Monoidal {suc 0ℓ} as System-⊗
+import Data.System.Monoidal as System-⊗
 import Categories.Morphism as Morphism
 import Functor.Free.Instance.SymmetricMonoidalPreorder.Strong as SymmetricMonoidalPreorder
 
@@ -26,7 +26,7 @@ open import Categories.Functor.Monoidal.Symmetric.Properties using (idF-StrongSy
 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.Construction.CMonoids (Setoids-×.symmetric {suc 0ℓ} {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)
@@ -35,8 +35,8 @@ open import Data.Product using (_,_; _×_)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
 open import Data.Setoid using (∣_∣)
 open import Data.Setoid.Unit using (⊤ₛ)
-open import Data.System {suc 0ℓ} using (System; _≤_; _≈_; Systems[_,_]; ≤-refl; ≤-trans; discrete; Systems-MC; Systems-SMC)
-open import Data.Values monoid using (module ≋; module Object; Values; ≋-isEquiv)
+open import Data.System using (System; _≤_; _≈_; Systems[_,_]; ≤-refl; ≤-trans; discrete; Systems-MC; Systems-SMC)
+open import Data.Values monoid using (module ≋; module Object; Values; ≋-isEquiv; module Algebra)
 open import Function using (Func; _⟶ₛ_; _⟨$⟩_; _∘_; id)
 open import Function.Construct.Identity using () renaming (function to Id)
 open import Function.Construct.Setoid using (_∙_)
@@ -62,7 +62,7 @@ private
 
 opaque
   unfolding Valuesₘ ≋-isEquiv
-  map : (Fin A → Fin B) → System A A → System B B
+  map : (Fin A → Fin B) → System (Values A) (Algebra.Valuesₘ A) → System (Values B) (Algebra.Valuesₘ B)
   map {A} {B} f X = let open System X in record
       { S = S
       ; fₛ = fₛ ∙ arr (Pull.₁ f)
@@ -72,7 +72,7 @@ opaque
 opaque
   unfolding map
   open System
-  map-≤ : (f : Fin A → Fin B) {X Y : System A A} → X ≤ Y → map f X ≤ map f Y
+  map-≤ : (f : Fin A → Fin B) {X Y : System (Values A) (Algebra.Valuesₘ A)} → X ≤ Y → map f X ≤ map f Y
   ⇒S (map-≤ f x≤y) = ⇒S x≤y
   ≗-fₛ (map-≤ f x≤y) = ≗-fₛ x≤y ∘ to (arr (Pull.₁ f))
   ≗-fₒ (map-≤ f x≤y) = cong (arr (Push.₁ f)) ∘ ≗-fₒ x≤y
@@ -81,15 +81,15 @@ opaque
   unfolding map-≤
   map-≤-refl
       : (f : Fin A → Fin B)
-      → {X : System A A}
-      → map-≤ f (≤-refl {A} {A} {X}) ≈ ≤-refl
+      → {X : System (Values A) (Algebra.Valuesₘ A)}
+      → map-≤ f (≤-refl {x = X}) ≈ ≤-refl
   map-≤-refl f {X} = Setoid.refl (S (map f X))
 
 opaque
   unfolding map-≤
   map-≤-trans
       : (f : Fin A → Fin B)
-      → {X Y Z : System A A}
+      → {X Y Z : System (Values A) (Algebra.Valuesₘ A)}
       → {h : X ≤ Y}
       → {g : Y ≤ Z}
       → map-≤ f (≤-trans h g) ≈ ≤-trans (map-≤ f h) (map-≤ f g)
@@ -99,13 +99,13 @@ opaque
   unfolding map-≤
   map-≈
       : (f : Fin A → Fin B)
-      → {X Y : System A A}
+      → {X Y : System (Values A) (Algebra.Valuesₘ A)}
       → {g h : X ≤ Y}
       → h ≈ g
       → map-≤ f h ≈ map-≤ f g
   map-≈ f h≈g = h≈g
 
-Sys₁ : (Fin A → Fin B) → Functor Systems[ A , A ] Systems[ B , B ]
+Sys₁ : (Fin A → Fin B) → Functor Systems[ Values A , Algebra.Valuesₘ A ] Systems[ Values B , Algebra.Valuesₘ B ]
 Sys₁ {A} {B} f = record
     { F₀ = map f
     ; F₁ = λ C≤D → map-≤ f C≤D
@@ -116,14 +116,14 @@ Sys₁ {A} {B} f = record
 
 opaque
   unfolding map
-  map-id-≤ : (X : System A A) → map id X ≤ X
+  map-id-≤ : (X : System (Values A) (Algebra.Valuesₘ A)) → map id X ≤ X
   map-id-≤ X .⇒S = Id (S X)
   map-id-≤ X .≗-fₛ i s = cong (fₛ X) Pull.identity
   map-id-≤ X .≗-fₒ s = Push.identity
 
 opaque
   unfolding map
-  map-id-≥ : (X : System A A) → X ≤ map id X
+  map-id-≥ : (X : System (Values A) (Algebra.Valuesₘ A)) → X ≤ map id X
   map-id-≥ X .⇒S = Id (S X)
   map-id-≥ X .≗-fₛ i s = cong (fₛ X) (≋.sym Pull.identity)
   map-id-≥ X .≗-fₒ s = ≋.sym Push.identity
@@ -131,7 +131,7 @@ opaque
 opaque
   unfolding map-≤ map-id-≤
   map-id-comm
-      : {X Y : System A A}
+      : {X Y : System (Values A) (Algebra.Valuesₘ A)}
         (f : X ≤ Y)
       → ≤-trans (map-≤ id f) (map-id-≤ Y) ≈ ≤-trans (map-id-≤ X) f
   map-id-comm {Y} f = Setoid.refl (S Y)
@@ -141,12 +141,12 @@ opaque
   unfolding map-id-≤ map-id-≥
 
   map-id-isoˡ
-      : (X : System A A)
+      : (X : System (Values A) (Algebra.Valuesₘ A))
       → ≤-trans (map-id-≤ X) (map-id-≥ X) ≈ ≤-refl
   map-id-isoˡ X = Setoid.refl (S X)
 
   map-id-isoʳ
-      : (X : System A A)
+      : (X : System (Values A) (Algebra.Valuesₘ A))
       → ≤-trans (map-id-≥ X) (map-id-≤ X) ≈ ≤-refl
   map-id-isoʳ X = Setoid.refl (S X)
 
@@ -166,7 +166,7 @@ opaque
   map-∘-≤
       : (f : Fin A → Fin B)
         (g : Fin B → Fin C)
-        (X : System A A)
+        (X : System (Values A) (Algebra.Valuesₘ A))
       → map (g ∘ f) X ≤ map g (map f X)
   map-∘-≤ f g X .⇒S = Id (S X)
   map-∘-≤ f g X .≗-fₛ i s = cong (fₛ X) Pull.homomorphism
@@ -177,7 +177,7 @@ opaque
   map-∘-≥
       : (f : Fin A → Fin B)
         (g : Fin B → Fin C)
-        (X : System A A)
+        (X : System (Values A) (Algebra.Valuesₘ A))
       → map g (map f X) ≤ map (g ∘ f) X
   map-∘-≥ f g X .⇒S = Id (S X)
   map-∘-≥ f g X .≗-fₛ i s = cong (fₛ X) (≋.sym Pull.homomorphism)
@@ -202,12 +202,12 @@ Sys-homo {A} f g = niHelper record
       map-∘-comm
           : (f : Fin A → Fin B)
             (g : Fin B → Fin C)
-          → {X Y : System A A}
+          → {X Y : System (Values A) (Algebra.Valuesₘ A)}
             (X≤Y : X ≤ Y)
           → ≤-trans (map-≤ (g ∘ f) X≤Y) (map-∘-≤ f g Y)
           ≈ ≤-trans (map-∘-≤ f g X) (map-≤ g (map-≤ f X≤Y))
       map-∘-comm f g {Y} X≤Y = Setoid.refl (S Y)
-    module _ (X : System A A) where
+    module _ (X : System (Values A) (Algebra.Valuesₘ A)) where
       opaque
         unfolding map-∘-≤ map-∘-≥
         isoˡ : ≤-trans (map-∘-≤ f g X) (map-∘-≥ f g X) ≈ ≤-refl
@@ -215,7 +215,7 @@ Sys-homo {A} f g = niHelper record
         isoʳ : ≤-trans (map-∘-≥ f g X) (map-∘-≤ f g X) ≈ ≤-refl
         isoʳ = Setoid.refl (S X)
 
-module _ {f g : Fin A → Fin B} (f≗g : f ≗ g) (X : System A A) where
+module _ {f g : Fin A → Fin B} (f≗g : f ≗ g) (X : System (Values A) (Algebra.Valuesₘ A)) where
 
   opaque
 
@@ -236,7 +236,7 @@ opaque
   map-cong-comm
       : {f g : Fin A → Fin B}
         (f≗g : f ≗ g)
-        {X Y : System A A}
+        {X Y : System (Values A) (Algebra.Valuesₘ A)}
         (h : X ≤ Y)
       → ≤-trans (map-≤ f h) (map-cong-≤ f≗g Y)
       ≈ ≤-trans (map-cong-≤ f≗g X) (map-≤ g h)
@@ -249,14 +249,14 @@ opaque
   map-cong-isoˡ
       : {f g : Fin A → Fin B}
         (f≗g : f ≗ g)
-        (X : System A A)
+        (X : System (Values A) (Algebra.Valuesₘ A))
       → ≤-trans (map-cong-≤ f≗g X) (map-cong-≥ f≗g X) ≈ ≤-refl
   map-cong-isoˡ f≗g X = Setoid.refl (S X)
 
   map-cong-isoʳ
       : {f g : Fin A → Fin B}
         (f≗g : f ≗ g)
-        (X : System A A)
+        (X : System (Values A) (Algebra.Valuesₘ A))
       → ≤-trans (map-cong-≥ f≗g X) (map-cong-≤ f≗g X) ≈ ≤-refl
   map-cong-isoʳ f≗g X = Setoid.refl (S X)
 
@@ -273,8 +273,8 @@ Sys-resp-≈ f≗g = niHelper record
 
 module NatCat where
 
-  Sys : Functor Nat (Cats (suc 0ℓ) (suc 0ℓ) 0ℓ)
-  Sys .F₀ n = Systems[ n , n ]
+  Sys : Functor Nat (Cats (suc 0ℓ) 0ℓ 0ℓ)
+  Sys .F₀ n = Systems[ Values n , Algebra.Valuesₘ n ]
   Sys .F₁ = Sys₁
   Sys .identity = Sys-identity
   Sys .homomorphism = Sys-homo _ _
@@ -286,15 +286,15 @@ module NatMC where
 
   module _ (f : Fin A → Fin B) where
 
-    module A = System-⊗ A A
-    module B = System-⊗ B B
+    module A = System-⊗ (Values A) (Algebra.Valuesₘ A)
+    module B = System-⊗ (Values B) (Algebra.Valuesₘ B)
 
     open CommutativeMonoid⇒ (Push.₁ f)
-    open Morphism Systems[ B , B ] using (_≅_)
+    open Morphism Systems[ Values B , Algebra.Valuesₘ B ] using (_≅_)
 
     opaque
       unfolding map
-      ε-≅ : discrete B B ≅ map f (discrete A A)
+      ε-≅ : discrete (Values B) (Algebra.Valuesₘ B) ≅ map f (discrete (Values A) (Algebra.Valuesₘ A))
       ε-≅ = record
           -- other fields can be inferred
           { from = record
@@ -335,7 +335,7 @@ module NatMC where
       module A-MC = MonoidalCategory A.Systems-MC
       module B-MC = MonoidalCategory B.Systems-MC
 
-      F : Functor Systems[ A , A ] Systems[ B , B ]
+      F : Functor Systems[ Values A , Algebra.Valuesₘ A ] Systems[ Values B , Algebra.Valuesₘ B ]
       F = Sys₁ f
 
       module F = Functor F
@@ -347,7 +347,7 @@ module NatMC where
       unfolding ⊗-homo-≃
 
       associativity
-          : {X Y Z : System A A}
+          : {X Y Z : System (Values A) (Algebra.Valuesₘ A)}
           → F.₁ A.Associator.assoc-≤
           ∘′ ⊗-homo-≃.⇒.η (X A.⊗₀ Y , Z)
           ∘′ ⊗-homo-≃.⇒.η (X , Y) B.⊗₁ B-MC.id
@@ -357,7 +357,7 @@ module NatMC where
       associativity {X} {Y} {Z} = Setoid.refl (S X ×ₛ (S Y ×ₛ S Z))
 
       unitaryˡ
-          : {X : System A A}
+          : {X : System (Values A) (Algebra.Valuesₘ A)}
           →  F.₁ A.Unitors.⊗-discreteˡ-≤
           ∘′ ⊗-homo-≃.⇒.η (A-MC.unit , X)
           ∘′ ε-≅.from B.⊗₁ B-MC.id 
@@ -365,14 +365,14 @@ module NatMC where
       unitaryˡ {X} = Setoid.refl (S X)
 
       unitaryʳ
-          : {X : System A A}
+          : {X : System (Values A) (Algebra.Valuesₘ A)}
           →  F.₁ A.Unitors.⊗-discreteʳ-≤
-          ∘′ ⊗-homo-≃.⇒.η (X , discrete A A)
+          ∘′ ⊗-homo-≃.⇒.η (X , discrete (Values A) (Algebra.Valuesₘ A))
           ∘′ B-MC.id B.⊗₁ ε-≅.from
           B-MC.≈ B-MC.unitorʳ.from
       unitaryʳ {X} = Setoid.refl (S X)
 
-    Sys-MC₁ : StrongMonoidalFunctor (Systems-MC A A) (Systems-MC B B)
+    Sys-MC₁ : StrongMonoidalFunctor (Systems-MC (Values A) (Algebra.Valuesₘ A)) (Systems-MC (Values B) (Algebra.Valuesₘ B))
     Sys-MC₁ = record
         { F = Sys₁ f
         ; isStrongMonoidal = record
@@ -386,7 +386,7 @@ module NatMC where
 
   opaque
     unfolding map-id-≤ ⊗-homo-≃
-    Sys-MC-identity : MonoidalNaturalIsomorphism (Sys-MC₁ id) (idF-StrongMonoidal (Systems-MC A A))
+    Sys-MC-identity : MonoidalNaturalIsomorphism (Sys-MC₁ id) (idF-StrongMonoidal (Systems-MC (Values A) (Algebra.Valuesₘ A)))
     Sys-MC-identity = record
         { U = NatCat.Sys.identity
         ; F⇒G-isMonoidal = record
@@ -423,8 +423,8 @@ module NatMC where
             }
         }
 
-  Sys : Functor Nat (StrongMonoidals (suc 0ℓ) (suc 0ℓ) 0ℓ)
-  Sys .F₀ n = Systems-MC n n
+  Sys : Functor Nat (StrongMonoidals (suc 0ℓ) 0ℓ 0ℓ)
+  Sys .F₀ n = Systems-MC (Values n) (Algebra.Valuesₘ n)
   Sys .F₁ = Sys-MC₁
   Sys .identity = Sys-MC-identity
   Sys .homomorphism = Sys-MC-homomorphism
@@ -438,29 +438,29 @@ module NatSMC where
 
     private
 
-      module A = System-⊗ A A
-      module B = System-⊗ B B
+      module A = System-⊗ (Values A) (Algebra.Valuesₘ A)
+      module B = System-⊗ (Values B) (Algebra.Valuesₘ B)
       module A-SMC = SymmetricMonoidalCategory A.Systems-SMC
       module B-SMC = SymmetricMonoidalCategory B.Systems-SMC
 
-      F : Functor Systems[ A , A ] Systems[ B , B ]
+      F : Functor Systems[ Values A , Algebra.Valuesₘ A ] Systems[ Values B , Algebra.Valuesₘ B ]
       F = Sys₁ f
 
       module F = Functor F
 
-      F-MF : StrongMonoidalFunctor (Systems-MC A A) (Systems-MC B B)
+      F-MF : StrongMonoidalFunctor (Systems-MC (Values A) (Algebra.Valuesₘ A)) (Systems-MC (Values B) (Algebra.Valuesₘ B))
       F-MF = NatMC.Sys.₁ f
       module F-MF = StrongMonoidalFunctor F-MF
 
     opaque
       unfolding NatMC.⊗-homo-≃
       σ-compat
-          : {X Y : System A A}
+          : {X Y : System (Values A) (Algebra.Valuesₘ 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 A) (Systems-SMC B B)
+    Sys-SMC₁ : SymmetricMonoidalFunctor (Systems-SMC (Values A) (Algebra.Valuesₘ A)) (Systems-SMC (Values B) (Algebra.Valuesₘ B))
     Sys-SMC₁ = record
         { F-MF
         ; isBraidedMonoidal = record
@@ -469,7 +469,7 @@ module NatSMC where
             }
         }
 
-  Sys-SMC-identity : SymmetricMonoidalNaturalIsomorphism (Sys-SMC₁ id) (idF-StrongSymmetricMonoidal (Systems-SMC A A))
+  Sys-SMC-identity : SymmetricMonoidalNaturalIsomorphism (Sys-SMC₁ id) (idF-StrongSymmetricMonoidal (Systems-SMC (Values A) (Algebra.Valuesₘ A)))
   Sys-SMC-identity = record { MonoidalNaturalIsomorphism NatMC.Sys.identity }
 
   Sys-SMC-homomorphism
@@ -484,8 +484,8 @@ module NatSMC where
       → 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₀ n = Systems-SMC n n
+  Sys : Functor Nat SymMonCat
+  Sys .F₀ n = Systems-SMC (Values n) (Algebra.Valuesₘ n)
   Sys .F₁ = Sys-SMC₁
   Sys .identity = Sys-SMC-identity
   Sys .homomorphism = Sys-SMC-homomorphism
diff --git a/Functor/Instance/Nat/System/Looped.agda b/Functor/Instance/Nat/System/Looped.agda
new file mode 100644
index 0000000..86ebd81
--- /dev/null
+++ b/Functor/Instance/Nat/System/Looped.agda
@@ -0,0 +1,256 @@
+{-# OPTIONS --without-K --safe #-}
+{-# OPTIONS --hidden-argument-puns #-}
+{-# OPTIONS --lossy-unification #-}
+
+module Functor.Instance.Nat.System.Looped where
+
+open import Level using (suc; 0ℓ)
+
+import Data.System.Monoidal as System-⊗
+import Functor.Instance.Nat.System as Unlooped
+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.Instance.Cats using (Cats)
+open import Categories.Category.Instance.Monoidals using (StrongMonoidals)
+open import Categories.Category.Instance.Nat using (Nat)
+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 (_≃_; 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ℓ} {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.System using (System; _≤_; _≈_; Systems[_]; ≤-refl; ≤-trans; discrete)
+open import Data.System.Looped.Monoidal using (Systems-MC; Systems-SMC)
+open import Data.Values monoid using (module ≋; module Algebra; Values; ≋-isEquiv)
+open import Function using (Func; _⟶ₛ_; _⟨$⟩_; _∘_; 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 Functor
+open Strong₁ using (SymMonCat)
+open Strong₂ using (MonoidalNaturalIsomorphism)
+open Strong₃ using (SymmetricMonoidalFunctor)
+open Strong₄ using (SymmetricMonoidalNaturalIsomorphism)
+open Algebra using (Valuesₘ)
+
+private
+  variable A B C : ℕ
+
+opaque
+
+  unfolding ≋-isEquiv
+
+  Sys₁ : (Fin A → Fin B) → Functor Systems[ Valuesₘ A ] Systems[ Valuesₘ B ]
+  Sys₁ f = record { Functor (Unlooped.NatCat.Sys.₁ f) }
+
+  Sys-identity : Sys₁ {A} id ≃ idF
+  Sys-identity {A} = record
+      { F⇒G = record { NI.⇒ }
+      ; F⇐G = record { NI.⇐ }
+      ; iso = λ X → record { NI.iso X }
+      }
+    where
+      module NI = NaturalIsomorphism (Unlooped.NatCat.Sys.identity {A})
+
+  Sys-homo
+      : (f : Fin A → Fin B)
+        (g : Fin B → Fin C)
+      → Sys₁ (g ∘ f) ≃ Sys₁ g ∘F Sys₁ f
+  Sys-homo {A} f g = record
+      { F⇒G = record { NI.⇒ }
+      ; F⇐G = record { NI.⇐ }
+      ; iso = λ X → record { NI.iso X }
+      }
+    where
+      module NI = NaturalIsomorphism (Unlooped.NatCat.Sys.homomorphism {f = f} {g})
+
+  Sys-resp-≈ : {f g : Fin A → Fin B} → f ≗ g → Sys₁ f ≃ Sys₁ g
+  Sys-resp-≈ f≗g = record
+      { F⇒G = record { NI.⇒ }
+      ; F⇐G = record { NI.⇐ }
+      ; iso = λ X → record { NI.iso X }
+      }
+    where
+      module NI = NaturalIsomorphism (Unlooped.NatCat.Sys.F-resp-≈ f≗g)
+
+module NatCat where
+
+  Sys : Functor Nat (Cats (suc 0ℓ) 0ℓ 0ℓ)
+  Sys .F₀ = λ n → Systems[ Valuesₘ n ]
+  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 A
+    -- module B = System-⊗ B B
+
+    module MF = StrongMonoidalFunctor (Unlooped.NatMC.Sys.₁ f)
+
+    open Morphism using (_≅_; Iso)
+
+    opaque
+
+      unfolding Sys₁ ≋-isEquiv
+
+      Sys-MC₁ : StrongMonoidalFunctor (Systems-MC (Valuesₘ A)) (Systems-MC (Valuesₘ B))
+      Sys-MC₁ = record
+          { F = Sys₁ f
+          ; isStrongMonoidal = record
+              { ε = record
+                  { _≅_ MF.ε
+                  ; iso = record { Iso MF.ε.iso }
+                  }
+              ; ⊗-homo = record
+                  { F⇒G = record { MF.⊗-homo.⇒ }
+                  ; F⇐G = record { MF.⊗-homo.⇐ }
+                  ; iso = λ X → record { MF.⊗-homo.iso X }
+                  }
+              ; associativity = λ {X Y Z} → MF.associativity {X} {Y} {Z}
+              ; unitaryˡ = λ {X} → MF.unitaryˡ {X}
+              ; unitaryʳ = λ {X} → MF.unitaryʳ {X}
+              }
+          }
+
+  opaque
+
+    unfolding Sys-MC₁
+
+    Sys-MC-identity : MonoidalNaturalIsomorphism (Sys-MC₁ id) (idF-StrongMonoidal (Systems-MC (Valuesₘ A)))
+    Sys-MC-identity {A} = record
+        { U = record
+            { F⇒G = record { ⇒ }
+            ; F⇐G = record { ⇐ }
+            ; iso = λ X → record { iso X}
+            }
+        ; F⇒G-isMonoidal = record
+            { ε-compat = ε-compat
+            ; ⊗-homo-compat = λ {X Y} → ⊗-homo-compat {X} {Y}
+            }
+        }
+      where
+        open MonoidalNaturalIsomorphism (Unlooped.NatMC.Sys.identity {A})
+
+    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 {g} {f} = record
+        { U = record
+            { F⇒G = record { ⇒ }
+            ; F⇐G = record { ⇐ }
+            ; iso = λ X → record { iso X}
+            }
+        ; F⇒G-isMonoidal = record
+            { ε-compat = ε-compat
+            ; ⊗-homo-compat = λ {X Y} → ⊗-homo-compat {X} {Y}
+            }
+        }
+      where
+        open MonoidalNaturalIsomorphism (Unlooped.NatMC.Sys.homomorphism {f = f} {g})
+
+    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 = record
+            { F⇒G = record { ⇒ }
+            ; F⇐G = record { ⇐ }
+            ; iso = λ X → record { iso X}
+            }
+        ; F⇒G-isMonoidal = record
+            { ε-compat = ε-compat
+            ; ⊗-homo-compat = λ {X Y} → ⊗-homo-compat {X} {Y}
+            }
+        }
+      where
+        open MonoidalNaturalIsomorphism (Unlooped.NatMC.Sys.F-resp-≈ f≗g)
+
+  Sys : Functor Nat (StrongMonoidals (suc 0ℓ) 0ℓ 0ℓ)
+  Sys .F₀ = λ n → Systems-MC (Valuesₘ n)
+  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
+
+    F-MF : StrongMonoidalFunctor (Systems-MC (Valuesₘ A)) (Systems-MC (Valuesₘ B))
+    F-MF = NatMC.Sys.₁ f
+    module F-MF = StrongMonoidalFunctor F-MF
+
+    module SMF = SymmetricMonoidalFunctor (Unlooped.NatSMC.Sys.₁ f)
+
+    opaque
+
+      unfolding NatMC.Sys-MC₁
+
+      Sys-SMC₁ : SymmetricMonoidalFunctor (Systems-SMC (Valuesₘ A)) (Systems-SMC (Valuesₘ B))
+      Sys-SMC₁ = record
+          { F-MF
+          ; isBraidedMonoidal = record
+              { F-MF
+              ; braiding-compat = λ {X Y} → SMF.braiding-compat {X} {Y}
+              }
+          }
+
+  opaque
+
+    unfolding Sys-SMC₁
+
+    Sys-SMC-identity : SymmetricMonoidalNaturalIsomorphism (Sys-SMC₁ id) (idF-StrongSymmetricMonoidal (Systems-SMC (Valuesₘ 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ℓ} {0ℓ} {0ℓ})
+    Sys .F₀ = λ n → Systems-SMC (Valuesₘ n)
+    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