aboutsummaryrefslogtreecommitdiff
path: root/Functor/Monoidal/Construction/MultisetOf.agda
diff options
context:
space:
mode:
authorJacques Comeaux <jacquesrcomeaux@protonmail.com>2025-11-09 20:28:11 -0600
committerJacques Comeaux <jacquesrcomeaux@protonmail.com>2025-11-09 20:28:11 -0600
commited5f0ae0f95a1675b272b205bb58724368031c01 (patch)
tree9b0cbe733a77d83050b665fe984a6e21c64a3815 /Functor/Monoidal/Construction/MultisetOf.agda
parent6a5154cf29d98ab644b5def52c55f213d1076e2b (diff)
Use functional vector in edge definition
Diffstat (limited to 'Functor/Monoidal/Construction/MultisetOf.agda')
-rw-r--r--Functor/Monoidal/Construction/MultisetOf.agda6
1 files changed, 3 insertions, 3 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 = ++-⊗-σ
}