diff options
| -rw-r--r-- | Data/System/Category.agda | 20 | ||||
| -rw-r--r-- | Data/System/Core.agda | 57 | ||||
| -rw-r--r-- | Data/System/Looped.agda | 105 | ||||
| -rw-r--r-- | Data/System/Looped/Monoidal.agda | 36 | ||||
| -rw-r--r-- | Data/System/Monoidal.agda | 78 | ||||
| -rw-r--r-- | Functor/Instance/Nat/System.agda | 96 | ||||
| -rw-r--r-- | Functor/Instance/Nat/System/Looped.agda | 256 |
7 files changed, 463 insertions, 185 deletions
diff --git a/Data/System/Category.agda b/Data/System/Category.agda index 171a003..50d950b 100644 --- a/Data/System/Category.agda +++ b/Data/System/Category.agda @@ -1,15 +1,15 @@ {-# OPTIONS --without-K --safe #-} -open import Level using (Level; 0ℓ; suc) +open import Level using (Level; suc; _⊔_) -module Data.System.Category {ℓ : Level} where +module Data.System.Category {c ℓ : Level} where import Relation.Binary.Reasoning.Setoid as ≈-Reasoning +open import Algebra using (CommutativeMonoid) open import Categories.Category using (Category) -open import Data.Nat using (ℕ) -open import Data.System.Core {ℓ} using (System; _≤_; ≤-trans; ≤-refl) open import Data.Setoid using (_⇒ₛ_) +open import Data.System.Core using (System; _≤_; ≤-trans; ≤-refl) open import Function using (Func; _⟨$⟩_; flip) open import Relation.Binary as Rel using (Setoid; Rel) @@ -17,13 +17,13 @@ open Func open System open _≤_ -private module ≈ {n m : ℕ} where +private module ≈ {I : Setoid c ℓ} {O : CommutativeMonoid c ℓ} where private variable - A B C : System n m + A B C : System I O - _≈_ : Rel (A ≤ B) 0ℓ + _≈_ : Rel (A ≤ B) ℓ _≈_ {A} {B} ≤₁ ≤₂ = ⇒S ≤₁ A⇒B.≈ ⇒S ≤₂ where module A⇒B = Setoid (S A ⇒ₛ S B) @@ -46,9 +46,9 @@ private module ≈ {n m : ℕ} where open ≈ using (_≈_) public open ≈ using (≈-isEquiv; ≤-resp-≈) -Systems[_,_] : ℕ → ℕ → Category (suc 0ℓ) ℓ 0ℓ -Systems[ n , m ] = record - { Obj = System n m +Systems[_,_] : Setoid c ℓ → CommutativeMonoid c ℓ → Category (c ⊔ suc ℓ) (c ⊔ ℓ) ℓ +Systems[ I , O ] = record + { Obj = System I O ; _⇒_ = _≤_ ; _≈_ = _≈_ ; id = ≤-refl diff --git a/Data/System/Core.agda b/Data/System/Core.agda index 3616847..d64045a 100644 --- a/Data/System/Core.agda +++ b/Data/System/Core.agda @@ -1,16 +1,14 @@ {-# OPTIONS --without-K --safe #-} -open import Level using (Level; 0ℓ; suc) +open import Level using (Level; 0ℓ; suc; _⊔_) -module Data.System.Core {ℓ : Level} where +module Data.System.Core {c ℓ : Level} where import Relation.Binary.Reasoning.Setoid as ≈-Reasoning -open import Data.Circuit.Value using (monoid) -open import Data.Nat using (ℕ) +open import Algebra using (CommutativeMonoid) open import Data.Setoid using (_⇒ₛ_; ∣_∣) open import Data.Setoid.Unit using (⊤ₛ) -open import Data.Values monoid using (Values; _≋_; module ≋; <ε>) open import Function using (Func; _⟨$⟩_) open import Function.Construct.Constant using () renaming (function to Const) open import Function.Construct.Identity using () renaming (function to Id) @@ -22,34 +20,49 @@ open Func -- A dynamical system with a set of states, -- a state update function, -- and a readout function -record System (n m : ℕ) : Set₁ where + +-- Really, the input type should be a cocommutative comonoid, +-- but every setoid is a cocommutative comonoid in a unique way +record System (I : Setoid c ℓ) (O : CommutativeMonoid c ℓ) : Set (c ⊔ suc ℓ) where + + private + module I = Setoid I + module O = CommutativeMonoid O field - S : Setoid 0ℓ 0ℓ - fₛ : ∣ Values n ⇒ₛ S ⇒ₛ S ∣ - fₒ : ∣ S ⇒ₛ Values m ∣ + S : Setoid ℓ ℓ + fₛ : ∣ I ⇒ₛ S ⇒ₛ S ∣ + fₒ : ∣ S ⇒ₛ O.setoid ∣ - fₛ′ : ∣ Values n ∣ → ∣ S ∣ → ∣ S ∣ + fₛ′ : I.Carrier → ∣ S ∣ → ∣ S ∣ fₛ′ i = to (to fₛ i) - fₒ′ : ∣ S ∣ → ∣ Values m ∣ + fₒ′ : ∣ S ∣ → O.Carrier fₒ′ = to fₒ module S = Setoid S open System --- the discrete system from n nodes to m nodes -discrete : (n m : ℕ) → System n m -discrete _ _ .S = ⊤ₛ -discrete n _ .fₛ = Const (Values n) (⊤ₛ ⇒ₛ ⊤ₛ) (Id ⊤ₛ) -discrete _ m .fₒ = Const ⊤ₛ (Values m) <ε> +module _ where + + open CommutativeMonoid + + -- the discrete system ignores input and outputs default value + discrete : (I : Setoid c ℓ) (O : CommutativeMonoid c ℓ) → System I O + discrete _ _ .S = ⊤ₛ + discrete I _ .fₛ = Const I (⊤ₛ ⇒ₛ ⊤ₛ) (Id ⊤ₛ) + discrete _ O .fₒ = Const ⊤ₛ (setoid O) (ε O) + +module _ {I : Setoid c ℓ} {O : CommutativeMonoid c ℓ} where -module _ {n m : ℕ} where + private + module I = Setoid I + module O = CommutativeMonoid O -- Simulation of systems: a mapping of internal -- states which respects i/o behavior - record _≤_ (A B : System n m) : Set ℓ where + record _≤_ (A B : System I O) : Set (c ⊔ ℓ) where private module A = System A @@ -57,8 +70,8 @@ module _ {n m : ℕ} where field ⇒S : ∣ A.S ⇒ₛ B.S ∣ - ≗-fₛ : (i : ∣ Values n ∣) (s : ∣ A.S ∣) → ⇒S ⟨$⟩ (A.fₛ′ i s) B.S.≈ B.fₛ′ i (⇒S ⟨$⟩ s) - ≗-fₒ : (s : ∣ A.S ∣) → A.fₒ′ s ≋ B.fₒ′ (⇒S ⟨$⟩ s) + ≗-fₛ : (i : I.Carrier) (s : ∣ A.S ∣) → ⇒S ⟨$⟩ (A.fₛ′ i s) B.S.≈ B.fₛ′ i (⇒S ⟨$⟩ s) + ≗-fₒ : (s : ∣ A.S ∣) → A.fₒ′ s O.≈ B.fₒ′ (⇒S ⟨$⟩ s) infix 4 _≤_ @@ -69,7 +82,7 @@ module _ {n m : ℕ} where ≤-refl : Reflexive _≤_ ⇒S ≤-refl = Id _ ≗-fₛ (≤-refl {x}) _ _ = S.refl x - ≗-fₒ ≤-refl _ = ≋.refl + ≗-fₒ ≤-refl _ = O.refl -- ≤ is transitive: if B simulates A, and C simulates B, then C simulates A ≤-trans : Transitive _≤_ @@ -78,7 +91,7 @@ module _ {n m : ℕ} where ⇒S b ⟨$⟩ (⇒S a ⟨$⟩ (fₛ′ x i s)) ≈⟨ cong (⇒S b) (≗-fₛ a i s) ⟩ ⇒S b ⟨$⟩ (fₛ′ y i (⇒S a ⟨$⟩ s)) ≈⟨ ≗-fₛ b i (⇒S a ⟨$⟩ s) ⟩ fₛ′ z i (⇒S b ⟨$⟩ (⇒S a ⟨$⟩ s)) ∎ - ≗-fₒ (≤-trans {x} {y} {z} a b) s = let open ≈-Reasoning (Values m) in begin + ≗-fₒ (≤-trans {x} {y} {z} a b) s = let open ≈-Reasoning O.setoid in begin fₒ′ x s ≈⟨ ≗-fₒ a s ⟩ fₒ′ y (⇒S a ⟨$⟩ s) ≈⟨ ≗-fₒ b (⇒S a ⟨$⟩ s) ⟩ fₒ′ z (⇒S b ⟨$⟩ (⇒S a ⟨$⟩ s)) ∎ diff --git a/Data/System/Looped.agda b/Data/System/Looped.agda index 96f3432..1fd86d6 100644 --- a/Data/System/Looped.agda +++ b/Data/System/Looped.agda @@ -1,74 +1,79 @@ {-# OPTIONS --without-K --safe #-} -open import Level using (Level; 0ℓ; suc) +open import Level using (Level; suc; _⊔_) -module Data.System.Looped {ℓ : Level} where +module Data.System.Looped {c ℓ : Level} where import Relation.Binary.Reasoning.Setoid as ≈-Reasoning +open import Algebra using (CommutativeMonoid) open import Categories.Category using (Category) open import Categories.Category.Helper using (categoryHelper) open import Categories.Functor using (Functor) -open import Data.Nat using (ℕ) -open import Data.System.Category {ℓ} using (Systems[_,_]) -open import Data.System.Core {ℓ} using (System; _≤_) -open import Categories.Functor using (Functor) -open import Data.Circuit.Value using (monoid) -open import Data.Values monoid using (_⊕_; ⊕-cong; module ≋) -open import Relation.Binary using (Setoid) +open import Data.System.Category using (Systems[_,_]) +open import Data.System.Core using (System; _≤_) open import Function using (Func; _⟨$⟩_) renaming (id to idf) +open import Relation.Binary using (Setoid) open Func open System private - loop : {n : ℕ} → System n n → System n n - loop X = record - { S = X.S - ; fₛ = record - { to = λ i → record - { to = λ s → X.fₛ′ (i ⊕ X.fₒ′ s) s - ; cong = λ {s} {s′} ≈s → X.S.trans - (cong X.fₛ (⊕-cong ≋.refl (cong X.fₒ ≈s))) (cong (X.fₛ ⟨$⟩ (i ⊕ X.fₒ′ s′)) ≈s) - } - ; cong = λ ≋v → cong X.fₛ (⊕-cong ≋v ≋.refl) - } - ; fₒ = X.fₒ - } - where - module X = System X + module _ {V : CommutativeMonoid c ℓ} where - loop-≤ : {n : ℕ} {A B : System n n} → A ≤ B → loop A ≤ loop B - loop-≤ {_} {A} {B} A≤B = record - { ⇒S = A≤B.⇒S - ; ≗-fₛ = λ i s → begin - A≤B.⇒S ⟨$⟩ (fₛ′ (loop A) i s) ≈⟨ A≤B.≗-fₛ (i ⊕ A.fₒ′ s) s ⟩ - B.fₛ′ (i ⊕ A.fₒ′ s) (A≤B.⇒S ⟨$⟩ s) ≈⟨ cong B.fₛ (⊕-cong ≋.refl (A≤B.≗-fₒ s)) ⟩ - B.fₛ′ (i ⊕ B.fₒ′ (A≤B.⇒S ⟨$⟩ s)) (A≤B.⇒S ⟨$⟩ s) ∎ - ; ≗-fₒ = A≤B.≗-fₒ - } - where - module A = System A - module B = System B - open ≈-Reasoning B.S - module A≤B = _≤_ A≤B + open CommutativeMonoid V -Loop : (n : ℕ) → Functor Systems[ n , n ] Systems[ n , n ] -Loop n = record - { F₀ = loop - ; F₁ = loop-≤ - ; identity = λ {A} → Setoid.refl (S A) - ; homomorphism = λ {Z = Z} → Setoid.refl (S Z) - ; F-resp-≈ = idf - } + loop : System setoid V → System setoid V + loop X = record + { S = X.S + ; fₛ = record + { to = λ i → record + { to = λ s → X.fₛ′ (i ∙ X.fₒ′ s) s + ; cong = λ {s} {s′} ≈s → + X.S.trans + (cong X.fₛ (∙-cong refl (cong X.fₒ ≈s))) + (cong (X.fₛ ⟨$⟩ (i ∙ X.fₒ′ s′)) ≈s) + } + ; cong = λ ≈v → cong X.fₛ (∙-congʳ ≈v) + } + ; fₒ = X.fₒ + } + where + module X = System X -module _ (n : ℕ) where + loop-≤ : {A B : System setoid V} → A ≤ B → loop A ≤ loop B + loop-≤ {A} {B} A≤B = record + { ⇒S = A≤B.⇒S + ; ≗-fₛ = λ i s → begin + A≤B.⇒S ⟨$⟩ (fₛ′ (loop A) i s) ≈⟨ A≤B.≗-fₛ (i ∙ A.fₒ′ s) s ⟩ + B.fₛ′ (i ∙ A.fₒ′ s) (A≤B.⇒S ⟨$⟩ s) ≈⟨ cong B.fₛ (∙-cong refl (A≤B.≗-fₒ s)) ⟩ + B.fₛ′ (i ∙ B.fₒ′ (A≤B.⇒S ⟨$⟩ s)) (A≤B.⇒S ⟨$⟩ s) ∎ + ; ≗-fₒ = A≤B.≗-fₒ + } + where + module A = System A + module B = System B + open ≈-Reasoning B.S + module A≤B = _≤_ A≤B + +module _ (V : CommutativeMonoid c ℓ) where + + open CommutativeMonoid V using (setoid) + + Loop : Functor Systems[ setoid , V ] Systems[ setoid , V ] + Loop = record + { F₀ = loop + ; F₁ = loop-≤ + ; identity = λ {A} → Setoid.refl (S A) + ; homomorphism = λ {Z = Z} → Setoid.refl (S Z) + ; F-resp-≈ = idf + } - open Category Systems[ n , n ] - open Functor (Loop n) + open Category Systems[ setoid , V ] + open Functor Loop - Systems[_] : Category (suc 0ℓ) ℓ 0ℓ + Systems[_] : Category (c ⊔ suc ℓ) (c ⊔ ℓ) ℓ Systems[_] = categoryHelper record { Obj = Obj ; _⇒_ = _⇒_ diff --git a/Data/System/Looped/Monoidal.agda b/Data/System/Looped/Monoidal.agda index af3d77c..81d5f7d 100644 --- a/Data/System/Looped/Monoidal.agda +++ b/Data/System/Looped/Monoidal.agda @@ -1,28 +1,30 @@ {-# OPTIONS --without-K --safe #-} -open import Level using (Level; 0ℓ; suc) +open import Level using (Level; suc; _⊔_) -module Data.System.Looped.Monoidal {ℓ : Level} where +module Data.System.Looped.Monoidal {c ℓ : Level} where import Categories.Morphism as Morphism -import Data.System.Monoidal {ℓ} as Unlooped +import Data.System.Monoidal as Unlooped +open import Algebra using (CommutativeMonoid) open import Categories.Category.Monoidal using (Monoidal) open import Categories.Category.Monoidal.Symmetric using (Symmetric) open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_) open import Categories.Category.Monoidal.Bundle using (MonoidalCategory; SymmetricMonoidalCategory) open import Categories.Functor.Bifunctor using (Bifunctor; flip-bifunctor) -open import Data.Nat using (ℕ) -open import Data.System.Core {ℓ} using (System) -open import Data.System.Looped {ℓ} using (Systems[_]) +open import Data.System.Core using (System) +open import Data.System.Looped using (Systems[_]) -module _ (n : ℕ) where +module _ (V : CommutativeMonoid c ℓ) where private - module Systems-MC = MonoidalCategory (Unlooped.Systems-MC n n) + module V = CommutativeMonoid V - ⊗ : Bifunctor Systems[ n ] Systems[ n ] Systems[ n ] + module Systems-MC = MonoidalCategory (Unlooped.Systems-MC V.setoid V) + + ⊗ : Bifunctor Systems[ V ] Systems[ V ] Systems[ V ] ⊗ = record { F₀ = Systems-MC.⊗.₀ ; F₁ = Systems-MC.⊗.₁ @@ -31,9 +33,9 @@ module _ (n : ℕ) where ; F-resp-≈ = λ {f = f} {g} → Systems-MC.⊗.F-resp-≈ {f = f} {g} } - module _ {X : System n n} where + module _ {X : System V.setoid V} where - open Morphism Systems[ n ] using (_≅_; module Iso) + open Morphism Systems[ V ] using (_≅_; module Iso) open Systems-MC using (_⊗₀_) unitorˡ : Systems-MC.unit ⊗₀ X ≅ X @@ -56,13 +58,13 @@ module _ (n : ℕ) where } } - module _ {X Y Z : System n n} where + module _ {X Y Z : System V.setoid V} where module X = System X module Y = System Y module Z = System Z - open Morphism Systems[ n ] using (_≅_; module Iso) + open Morphism Systems[ V ] using (_≅_; module Iso) open Systems-MC using (_⊗₀_) associator : (X ⊗₀ Y) ⊗₀ Z ≅ X ⊗₀ (Y ⊗₀ Z) @@ -75,7 +77,7 @@ module _ (n : ℕ) where } } - Systems-Monoidal : Monoidal Systems[ n ] + Systems-Monoidal : Monoidal Systems[ V ] Systems-Monoidal = record { ⊗ = ⊗ ; unit = Systems-MC.unit @@ -94,7 +96,7 @@ module _ (n : ℕ) where private - module Systems-SMC = SymmetricMonoidalCategory (Unlooped.Systems-SMC n n) + module Systems-SMC = SymmetricMonoidalCategory (Unlooped.Systems-SMC V.setoid V) braiding : ⊗ ≃ flip-bifunctor ⊗ braiding = record @@ -113,8 +115,8 @@ module _ (n : ℕ) where ; commutative = λ {X Y} → Systems-SMC.commutative {X} {Y} } - Systems-MC : MonoidalCategory (suc 0ℓ) ℓ 0ℓ + Systems-MC : MonoidalCategory (c ⊔ suc ℓ) (c ⊔ ℓ) ℓ Systems-MC = record { monoidal = Systems-Monoidal } - Systems-SMC : SymmetricMonoidalCategory (suc 0ℓ) ℓ 0ℓ + Systems-SMC : SymmetricMonoidalCategory (c ⊔ suc ℓ) (c ⊔ ℓ) ℓ Systems-SMC = record { symmetric = Systems-Symmetric } diff --git a/Data/System/Monoidal.agda b/Data/System/Monoidal.agda index cdf06e2..1c24e07 100644 --- a/Data/System/Monoidal.agda +++ b/Data/System/Monoidal.agda @@ -1,46 +1,48 @@ {-# OPTIONS --without-K --safe #-} -open import Data.Nat using (ℕ) -open import Level using (Level; suc; 0ℓ) +open import Algebra using (CommutativeMonoid) +open import Level using (Level; suc; _⊔_) +open import Relation.Binary using (Setoid) -module Data.System.Monoidal {ℓ : Level} (n m : ℕ) where +module Data.System.Monoidal {c ℓ : Level} (I : Setoid c ℓ) (O : CommutativeMonoid c ℓ) where -open import Data.System.Core {ℓ} using (System; _≤_; ≤-refl; ≤-trans; discrete) -open import Data.System.Category {ℓ} using (Systems[_,_]) +open import Data.System.Core using (System; _≤_; ≤-refl; ≤-trans; discrete) +open import Data.System.Category using (Systems[_,_]) 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.Category.Monoidal.Symmetric using (Symmetric) open import Categories.Functor using (Functor) open import Categories.Functor.Bifunctor using (Bifunctor; flip-bifunctor) -open import Categories.Morphism (Systems[ n , m ]) using (_≅_; Iso) +open import Categories.Morphism (Systems[ I , O ]) 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.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 +private + module I = Setoid I + module O = CommutativeMonoid O + module _ where open Func - δₛ : Values n ⟶ₛ Values n ×ₛ Values n + δₛ : I ⟶ₛ I ×ₛ I δₛ .to v = v , v δₛ .cong v≋w = v≋w , v≋w - ⊕ₛ : Values m ×ₛ Values m ⟶ₛ Values m - ⊕ₛ .to (v , w) = v ⊕ w - ⊕ₛ .cong (v₁≋v₂ , w₁≋w₂) = ⊕-cong v₁≋v₂ w₁≋w₂ + ⊕ₛ : O.setoid ×ₛ O.setoid ⟶ₛ O.setoid + ⊕ₛ .to (v , w) = v O.∙ w + ⊕ₛ .cong (v₁≈v₂ , w₁≈w₂) = O.∙-cong v₁≈v₂ w₁≈w₂ -_⊗₀_ : System n m → System n m → System n m +_⊗₀_ : System I O → System I O → System I O _⊗₀_ X Y = let open System in record { S = S X ×ₛ S Y ; fₛ = fₛ X ×-⇒ fₛ Y ∙ δₛ @@ -48,60 +50,60 @@ _⊗₀_ X Y = let open System in record } _⊗₁_ - : {A A′ B B′ : System n m} + : {A A′ B B′ : System I O} (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₂) +_⊗₁_ f g .≗-fₒ (s₁ , s₂) = O.∙-cong (≗-fₒ f s₁) (≗-fₒ g s₂) module _ where open Functor open System - ⊗ : Bifunctor Systems[ n , m ] Systems[ n , m ] Systems[ n , m ] + ⊗ : Bifunctor Systems[ I , O ] Systems[ I , O ] Systems[ I , O ] ⊗ .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 m} where +module Unitors {X : System I O} where open System X - ⊗-discreteˡ-≤ : discrete n m ⊗₀ X ≤ X + ⊗-discreteˡ-≤ : discrete I O ⊗₀ X ≤ X ⊗-discreteˡ-≤ .⇒S = proj₂ₛ ⊗-discreteˡ-≤ .≗-fₛ i s = S.refl - ⊗-discreteˡ-≤ .≗-fₒ (_ , s) = ⊕-identityˡ (fₒ′ s) + ⊗-discreteˡ-≤ .≗-fₒ (_ , s) = O.identityˡ (fₒ′ s) - ⊗-discreteˡ-≥ : X ≤ discrete n m ⊗₀ X + ⊗-discreteˡ-≥ : X ≤ discrete I O ⊗₀ 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ˡ-≥ .≗-fₒ s = O.sym (O.identityˡ (fₒ′ s)) - ⊗-discreteʳ-≤ : X ⊗₀ discrete n m ≤ X + ⊗-discreteʳ-≤ : X ⊗₀ discrete I O ≤ X ⊗-discreteʳ-≤ .⇒S = proj₁ₛ ⊗-discreteʳ-≤ .≗-fₛ i s = S.refl - ⊗-discreteʳ-≤ .≗-fₒ (s , _) = ⊕-identityʳ (fₒ′ s) + ⊗-discreteʳ-≤ .≗-fₒ (s , _) = O.identityʳ (fₒ′ s) - ⊗-discreteʳ-≥ : X ≤ X ⊗₀ discrete n m + ⊗-discreteʳ-≥ : X ≤ X ⊗₀ discrete I O ⊗-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ʳ-≥ .≗-fₒ s = O.sym (O.identityʳ (fₒ′ s)) open _≅_ open Iso - unitorˡ : discrete n m ⊗₀ X ≅ X + unitorˡ : discrete I O ⊗₀ X ≅ X unitorˡ .from = ⊗-discreteˡ-≤ unitorˡ .to = ⊗-discreteˡ-≥ unitorˡ .iso .isoˡ = _ , S.refl unitorˡ .iso .isoʳ = S.refl - unitorʳ : X ⊗₀ discrete n m ≅ X + unitorʳ : X ⊗₀ discrete I O ≅ X unitorʳ .from = ⊗-discreteʳ-≤ unitorʳ .to = ⊗-discreteʳ-≥ unitorʳ .iso .isoˡ = S.refl , _ @@ -109,7 +111,7 @@ module Unitors {X : System n m} where open Unitors using (unitorˡ; unitorʳ) public -module Associator {X Y Z : System n m} where +module Associator {X Y Z : System I O} where module X = System X module Y = System Y @@ -118,12 +120,12 @@ module Associator {X Y Z : System n m} where 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-≤ .≗-fₒ ((s₁ , s₂) , s₃) = O.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₃) ) + assoc-≥ .≗-fₒ (s₁ , (s₂ , s₃)) = O.sym (O.assoc (X.fₒ′ s₁) (Y.fₒ′ s₂) (Z.fₒ′ s₃) ) open _≅_ open Iso @@ -136,10 +138,10 @@ module Associator {X Y Z : System n m} where open Associator using (associator) public -Systems-Monoidal : Monoidal Systems[ n , m ] +Systems-Monoidal : Monoidal Systems[ I , O ] Systems-Monoidal = let open System in record { ⊗ = ⊗ - ; unit = discrete n m + ; unit = discrete I O ; unitorˡ = unitorˡ ; unitorʳ = unitorʳ ; associator = associator @@ -155,10 +157,10 @@ Systems-Monoidal = let open System in record open System -⊗-swap-≤ : {X Y : System n m} → Y ⊗₀ X ≤ X ⊗₀ Y +⊗-swap-≤ : {X Y : System I O} → 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₂) +⊗-swap-≤ {X} {Y} .≗-fₒ (s₁ , s₂) = O.comm (fₒ′ Y s₁) (fₒ′ X s₂) braiding : ⊗ ≃ flip-bifunctor ⊗ braiding = niHelper record @@ -181,8 +183,8 @@ Systems-Symmetric = record ; commutative = λ {X} {Y} → refl (S Y) , refl (S X) } -Systems-MC : MonoidalCategory (suc 0ℓ) ℓ 0ℓ +Systems-MC : MonoidalCategory (c ⊔ suc ℓ) (c ⊔ ℓ) ℓ Systems-MC = record { monoidal = Systems-Monoidal } -Systems-SMC : SymmetricMonoidalCategory (suc 0ℓ) ℓ 0ℓ +Systems-SMC : SymmetricMonoidalCategory (c ⊔ suc ℓ) (c ⊔ ℓ) ℓ Systems-SMC = record { symmetric = Systems-Symmetric } 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 |