diff options
Diffstat (limited to 'Functor/Monoidal')
| -rw-r--r-- | Functor/Monoidal/Construction/MultisetOf.agda | 6 | ||||
| -rw-r--r-- | Functor/Monoidal/Instance/Nat/Circ.agda | 20 |
2 files changed, 13 insertions, 13 deletions
diff --git a/Functor/Monoidal/Construction/MultisetOf.agda b/Functor/Monoidal/Construction/MultisetOf.agda index eca7b3a..83bdf52 100644 --- a/Functor/Monoidal/Construction/MultisetOf.agda +++ b/Functor/Monoidal/Construction/MultisetOf.agda @@ -81,9 +81,9 @@ open SymmetricMonoidalFunctor module ListOf,++,[] = MonoidalFunctor ListOf,++,[] -BagOf,++,[] : SymmetricMonoidalFunctor 𝒞-SMC S -BagOf,++,[] .F = List∘G -BagOf,++,[] .isBraidedMonoidal = record +MultisetOf,++,[] : SymmetricMonoidalFunctor 𝒞-SMC S +MultisetOf,++,[] .F = List∘G +MultisetOf,++,[] .isBraidedMonoidal = record { isMonoidal = ListOf,++,[].isMonoidal ; braiding-compat = ++-⊗-σ } diff --git a/Functor/Monoidal/Instance/Nat/Circ.agda b/Functor/Monoidal/Instance/Nat/Circ.agda index 9d38127..0e2d3eb 100644 --- a/Functor/Monoidal/Instance/Nat/Circ.agda +++ b/Functor/Monoidal/Instance/Nat/Circ.agda @@ -46,29 +46,29 @@ Nat-Cocartesian-Category : CocartesianCategory 0ℓ 0ℓ 0ℓ Nat-Cocartesian-Category = record { cocartesian = Nat-Cocartesian } open import Functor.Monoidal.Construction.MultisetOf - {𝒞 = Nat-Cocartesian-Category} (Edge Gates) FreeCMonoid using (BagOf,++,[]) + {𝒞 = Nat-Cocartesian-Category} (Edge Gates) FreeCMonoid using (MultisetOf,++,[]) open Lax using (SymmetricMonoidalFunctor) -module BagOf,++,[] = SymmetricMonoidalFunctor BagOf,++,[] +module MultisetOf,++,[] = SymmetricMonoidalFunctor MultisetOf,++,[] open SymmetricMonoidalFunctor ε⇒ : SingletonSetoid ⟶ₛ Circuitₛ 0 -ε⇒ = mkCircuitₛ ∙ BagOf,++,[].ε +ε⇒ = mkCircuitₛ ∙ MultisetOf,++,[].ε open Cocartesian Nat-Cocartesian using (-+-) open Func η : {n m : ℕ} → Circuitₛ n ×ₛ Circuitₛ m ⟶ₛ Circuitₛ (n + m) -η {n} {m} .to (mkCircuit X , mkCircuit Y) = mkCircuit (BagOf,++,[].⊗-homo.η (n , m) ⟨$⟩ (X , Y)) -η {n} {m} .cong (mk≈ x , mk≈ y) = mk≈ (cong (BagOf,++,[].⊗-homo.η (n , m)) (x , y)) +η {n} {m} .to (mkCircuit X , mkCircuit Y) = mkCircuit (MultisetOf,++,[].⊗-homo.η (n , m) ⟨$⟩ (X , Y)) +η {n} {m} .cong (mk≈ x , mk≈ y) = mk≈ (cong (MultisetOf,++,[].⊗-homo.η (n , m)) (x , y)) ⊗-homomorphism : NaturalTransformation (-×- ∘F (Circ ⁂ Circ)) (Circ ∘F -+-) ⊗-homomorphism = ntHelper record { η = λ (n , m) → η {n} {m} - ; commute = λ { (f , g) {mkCircuit X , mkCircuit Y} → mk≈ (BagOf,++,[].⊗-homo.commute (f , g) {X , Y}) } + ; commute = λ { (f , g) {mkCircuit X , mkCircuit Y} → mk≈ (MultisetOf,++,[].⊗-homo.commute (f , g) {X , Y}) } } Circ,⊗,ε : SymmetricMonoidalFunctor Nat,+,0 Setoids-× @@ -78,10 +78,10 @@ Circ,⊗,ε .isBraidedMonoidal = record { ε = ε⇒ ; ⊗-homo = ⊗-homomorphism ; associativity = λ { {n} {m} {o} {(mkCircuit x , mkCircuit y) , mkCircuit z} → - mk≈ (BagOf,++,[].associativity {n} {m} {o} {(x , y) , z}) } - ; unitaryˡ = λ { {n} {_ , mkCircuit x} → mk≈ (BagOf,++,[].unitaryˡ {n} {_ , x}) } - ; unitaryʳ = λ { {n} {mkCircuit x , _} → mk≈ (BagOf,++,[].unitaryʳ {n} {x , _}) } + mk≈ (MultisetOf,++,[].associativity {n} {m} {o} {(x , y) , z}) } + ; unitaryˡ = λ { {n} {_ , mkCircuit x} → mk≈ (MultisetOf,++,[].unitaryˡ {n} {_ , x}) } + ; unitaryʳ = λ { {n} {mkCircuit x , _} → mk≈ (MultisetOf,++,[].unitaryʳ {n} {x , _}) } } ; braiding-compat = λ { {n} {m} {mkCircuit x , mkCircuit y} → - mk≈ (BagOf,++,[].braiding-compat {n} {m} {x , y}) } + mk≈ (MultisetOf,++,[].braiding-compat {n} {m} {x , y}) } } |