diff options
Diffstat (limited to 'Functor/Monoidal/Construction')
| -rw-r--r-- | Functor/Monoidal/Construction/MultisetOf.agda | 6 |
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 = ++-⊗-σ } |