From ed5f0ae0f95a1675b272b205bb58724368031c01 Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Sun, 9 Nov 2025 20:28:11 -0600
Subject: Use functional vector in edge definition

---
 Functor/Monoidal/Construction/MultisetOf.agda | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'Functor/Monoidal/Construction')

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 = ++-⊗-σ
     }
-- 
cgit v1.2.3