diff options
| author | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2025-11-09 20:28:11 -0600 |
|---|---|---|
| committer | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2025-11-09 20:28:11 -0600 |
| commit | ed5f0ae0f95a1675b272b205bb58724368031c01 (patch) | |
| tree | 9b0cbe733a77d83050b665fe984a6e21c64a3815 /Functor/Monoidal/Construction | |
| parent | 6a5154cf29d98ab644b5def52c55f213d1076e2b (diff) | |
Use functional vector in edge definition
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 = ++-⊗-σ } |