From 4e85ade36a25151021a74b51442dca999e1b48e2 Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Tue, 13 Jan 2026 17:34:50 -0600
Subject: Remove old multisetof construction

---
 Functor/Monoidal/Construction/MultisetOf.agda | 89 ---------------------------
 1 file changed, 89 deletions(-)
 delete mode 100644 Functor/Monoidal/Construction/MultisetOf.agda

(limited to 'Functor')

diff --git a/Functor/Monoidal/Construction/MultisetOf.agda b/Functor/Monoidal/Construction/MultisetOf.agda
deleted file mode 100644
index 83bdf52..0000000
--- a/Functor/Monoidal/Construction/MultisetOf.agda
+++ /dev/null
@@ -1,89 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-
-open import Categories.Category using (Category)
-open import Categories.Category.Cocartesian.Bundle using (CocartesianCategory)
-open import Categories.Category.Construction.Monoids using (Monoids)
-open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory)
-open import Categories.Functor using (Functor) renaming (_∘F_ to _∙_)
-open import Category.Construction.CMonoids using (CMonoids)
-
-open import Level using (Level)
-
-module Functor.Monoidal.Construction.MultisetOf
-    {o o′ ℓ ℓ′ e e′ : Level}
-    {𝒞 : CocartesianCategory o ℓ e}
-    {S : SymmetricMonoidalCategory o′ ℓ′ e′}
-    (let module 𝒞 = CocartesianCategory 𝒞)
-    (let module S = SymmetricMonoidalCategory S)
-    (G : Functor 𝒞.U S.U)
-    (M : Functor S.U (CMonoids S.symmetric))
-  where
-
-import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning
-import Categories.Category.Monoidal.Utilities as ⊗-Util
-import Categories.Morphism.Reasoning as ⇒-Reasoning
-import Object.Monoid.Commutative as CMonoidObject
-
-open import Categories.Category.Cocartesian using (module CocartesianSymmetricMonoidal)
-open import Categories.Category.Monoidal.Symmetric.Properties using (module Shorthands)
-open import Categories.Functor.Monoidal using (MonoidalFunctor)
-open import Categories.Functor.Monoidal.Symmetric using (module Lax)
-open import Categories.Functor.Properties using ([_]-resp-∘)
-open import Data.Product using (_,_)
-
-module G = Functor G
-module M = Functor M
-module 𝒞-SM = CocartesianSymmetricMonoidal 𝒞.U 𝒞.cocartesian
-
-open 𝒞 using (⊥; -+-; _+_; _+₁_; i₁; i₂; inject₁; inject₂; +-swap)
-open Lax using (SymmetricMonoidalFunctor)
-
-open S
-open Functor
-open CMonoidObject symmetric using (CommutativeMonoid; CommutativeMonoid⇒)
-open CommutativeMonoid renaming (assoc to μ-assoc; identityˡ to μ-identityˡ; identityʳ to μ-identityʳ; commutative to μ-commutative)
-open CommutativeMonoid⇒
-
-Forget : Functor (CMonoids symmetric) (Monoids monoidal)
-Forget .F₀ = monoid
-Forget .F₁ = monoid⇒
-Forget .identity = Equiv.refl
-Forget .homomorphism = Equiv.refl
-Forget .F-resp-≈ x = x
-
-𝒞-SMC : SymmetricMonoidalCategory o ℓ e
-𝒞-SMC = record { symmetric = 𝒞-SM.+-symmetric }
-
-open import Functor.Monoidal.Construction.ListOf {𝒞 = 𝒞} G (Forget ∙ M)
-    using (List∘G; ListOf,++,[]; module LG; ++; module List; ++⇒)
-
-open Shorthands symmetric
-
-++-swap : {A : Obj} → ++ {A} ≈ ++ ∘ σ⇒
-++-swap {A} = μ-commutative (M.₀ A)
-
-open ⇒-Reasoning U
-open ⊗-Reasoning monoidal
-
-++-⊗-σ
-    : {X Y : 𝒞.Obj}
-    → LG.₁ (+-swap {X} {Y}) ∘ ++ ∘ LG.₁ i₁ ⊗₁ LG.₁ i₂
-    ≈ (++ ∘ LG.₁ i₁ ⊗₁ LG.₁ i₂) ∘ σ⇒
-++-⊗-σ {X} {Y} = begin
-    LG.₁ +-swap ∘ ++ ∘ LG.₁ i₁ ⊗₁ LG.₁ i₂                   ≈⟨ extendʳ (++⇒ (G.₁ +-swap)) ⟩
-    ++ ∘ LG.₁ +-swap ⊗₁ LG.₁ +-swap ∘ LG.₁ i₁ ⊗₁ LG.₁ i₂    ≈⟨ refl⟩∘⟨ ⊗-distrib-over-∘ ⟨
-    ++ ∘ (LG.₁ +-swap ∘ LG.₁ i₁) ⊗₁ (LG.₁ +-swap ∘ LG.₁ i₂) ≈⟨ refl⟩∘⟨ [ List∘G ]-resp-∘ inject₁ ⟩⊗⟨ [ List∘G ]-resp-∘ inject₂ ⟩
-    ++ ∘ LG.₁ i₂ ⊗₁ LG.₁ i₁                                 ≈⟨ pushˡ ++-swap ⟩
-    ++ ∘ σ⇒ ∘ LG.₁ i₂ ⊗₁ LG.₁ i₁                            ≈⟨ pushʳ (braiding.⇒.commute (LG.₁ i₂ , LG.₁ i₁ )) ⟩
-    (++ ∘ LG.₁ i₁ ⊗₁ LG.₁ i₂) ∘ σ⇒                          ∎
-
-open SymmetricMonoidalFunctor
-
-module ListOf,++,[] = MonoidalFunctor ListOf,++,[]
-
-MultisetOf,++,[] : SymmetricMonoidalFunctor 𝒞-SMC S
-MultisetOf,++,[] .F = List∘G
-MultisetOf,++,[] .isBraidedMonoidal = record
-    { isMonoidal = ListOf,++,[].isMonoidal
-    ; braiding-compat = ++-⊗-σ
-    }
-- 
cgit v1.2.3