From 8ec259bb32b4339b27560f5ea13afa81b9b8febc Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Wed, 7 Jan 2026 10:12:13 -0600
Subject: Differentiate lax and strong monoidal monotones

---
 Category/Instance/SymMonPre/Primitive.agda | 83 ------------------------------
 1 file changed, 83 deletions(-)
 delete mode 100644 Category/Instance/SymMonPre/Primitive.agda

(limited to 'Category/Instance/SymMonPre/Primitive.agda')

diff --git a/Category/Instance/SymMonPre/Primitive.agda b/Category/Instance/SymMonPre/Primitive.agda
deleted file mode 100644
index 7475719..0000000
--- a/Category/Instance/SymMonPre/Primitive.agda
+++ /dev/null
@@ -1,83 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-
-module Category.Instance.SymMonPre.Primitive where
-
-import Category.Instance.MonoidalPreorders.Primitive as MP using (_≃_; module ≃)
-
-open import Categories.Category using (Category)
-open import Categories.Category.Helper using (categoryHelper)
-open import Category.Instance.MonoidalPreorders.Primitive using (MonoidalPreorders)
-open import Level using (Level; suc; _⊔_)
-open import Preorder.Primitive.Monoidal using (SymmetricMonoidalPreorder; SymmetricMonoidalMonotone)
-open import Relation.Binary using (IsEquivalence)
-
-module _ {c₁ c₂ ℓ₁ ℓ₂ : Level} {A : SymmetricMonoidalPreorder c₁ ℓ₁} {B : SymmetricMonoidalPreorder c₂ ℓ₂} where
-
-  open SymmetricMonoidalMonotone using () renaming (monoidalMonotone to mM)
-
-  -- Pointwise isomorphism of symmetric monoidal monotone maps
-  _≃_ : (f g : SymmetricMonoidalMonotone A B) → Set (c₁ ⊔ ℓ₂)
-  f ≃ g = mM f MP.≃ mM g
-
-  infix 4 _≃_
-
-  ≃-isEquivalence : IsEquivalence _≃_
-  ≃-isEquivalence = let open MP.≃ in record
-      { refl = λ {x} → refl {x = mM x}
-      ; sym = λ {f g} → sym {x = mM f} {y = mM g}
-      ; trans = λ {f g h} → trans {i = mM f} {j = mM g} {k = mM h}
-      }
-
-  module ≃ = IsEquivalence ≃-isEquivalence
-
-private
-
-  identity : {c ℓ : Level} (A : SymmetricMonoidalPreorder c ℓ) → SymmetricMonoidalMonotone A A
-  identity {c} {ℓ} A = record
-      { monoidalMonotone = id {monoidalPreorder}
-      }
-    where
-      open SymmetricMonoidalPreorder A using (monoidalPreorder)
-      open Category (MonoidalPreorders c ℓ) using (id)
-
-  compose
-      : {c ℓ : Level}
-        {P Q R : SymmetricMonoidalPreorder c ℓ}
-      → SymmetricMonoidalMonotone Q R
-      → SymmetricMonoidalMonotone P Q
-      → SymmetricMonoidalMonotone P R
-  compose {c} {ℓ} {R = R} G F = record
-      { monoidalMonotone = G.monoidalMonotone ∘ F.monoidalMonotone
-      }
-    where
-      module G = SymmetricMonoidalMonotone G
-      module F = SymmetricMonoidalMonotone F
-      open Category (MonoidalPreorders c ℓ) using (_∘_)
-
-  compose-resp-≃
-      : {c ℓ : Level}
-        {A B C : SymmetricMonoidalPreorder c ℓ}
-        {f h : SymmetricMonoidalMonotone B C}
-        {g i : SymmetricMonoidalMonotone A B}
-      → f ≃ h
-      → g ≃ i
-      → compose f g ≃ compose h i
-  compose-resp-≃ {C = C} {f = f} {g} {h} {i} = ∘-resp-≈ {f = mM f} {mM g} {mM h} {mM i}
-    where
-      open Category (MonoidalPreorders _ _)
-      open SymmetricMonoidalMonotone using () renaming (monoidalMonotone to mM)
-
--- The category of symmetric monoidal preorders
-SymMonPre : (c ℓ : Level) → Category (suc (c ⊔ ℓ)) (c ⊔ ℓ) (c ⊔ ℓ)
-SymMonPre c ℓ = categoryHelper record
-    { Obj = SymmetricMonoidalPreorder c ℓ
-    ; _⇒_ = SymmetricMonoidalMonotone
-    ; _≈_ = _≃_
-    ; id  = λ {A} → identity A
-    ; _∘_ = compose
-    ; assoc = λ {f = f} {g h} → ≃.refl {x = compose (compose h g) f}
-    ; identityˡ = λ {f = f} → ≃.refl {x = f}
-    ; identityʳ = λ {f = f} → ≃.refl {x = f}
-    ; equiv = ≃-isEquivalence
-    ; ∘-resp-≈ = λ {f = f} {g h i} → compose-resp-≃ {f = f} {g} {h} {i}
-    }
-- 
cgit v1.2.3