From 05a7c242d961851ee0085359a44c989489beacd0 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Sat, 10 Jan 2026 22:08:08 -0600 Subject: Define Sys functor from Nat to SMCs --- Data/Setoid.agda | 44 ++++++- Data/System/Monoidal.agda | 187 ++++++++++++++++++++++++++ Functor/Instance/Nat/Push.agda | 114 ++++++++-------- Functor/Instance/Nat/System.agda | 277 ++++++++++++++++++++++++++++++++++++--- 4 files changed, 547 insertions(+), 75 deletions(-) create mode 100644 Data/System/Monoidal.agda 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 -- cgit v1.2.3