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/MonoidalPreorders/Primitive.agda | 86 ----------------------
 1 file changed, 86 deletions(-)
 delete mode 100644 Category/Instance/MonoidalPreorders/Primitive.agda

(limited to 'Category/Instance/MonoidalPreorders')

diff --git a/Category/Instance/MonoidalPreorders/Primitive.agda b/Category/Instance/MonoidalPreorders/Primitive.agda
deleted file mode 100644
index d00e17a..0000000
--- a/Category/Instance/MonoidalPreorders/Primitive.agda
+++ /dev/null
@@ -1,86 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-
-module Category.Instance.MonoidalPreorders.Primitive where
-
-import Preorder.Primitive.MonotoneMap as MonotoneMap using (_≃_; module ≃)
-
-open import Categories.Category using (Category)
-open import Categories.Category.Helper using (categoryHelper)
-open import Category.Instance.Preorders.Primitive using (Preorders)
-open import Level using (Level; suc; _⊔_)
-open import Preorder.Primitive.Monoidal using (MonoidalPreorder; MonoidalMonotone)
-open import Relation.Binary using (IsEquivalence)
-
-module _ {c₁ c₂ ℓ₁ ℓ₂ : Level} {A : MonoidalPreorder c₁ ℓ₁} {B : MonoidalPreorder c₂ ℓ₂} where
-
-  -- Pointwise equality of monoidal monotone maps
-
-  open MonoidalMonotone using (F)
-
-  _≃_ : (f g : MonoidalMonotone A B) → Set (c₁ ⊔ ℓ₂)
-  f ≃ g = F f MonotoneMap.≃ F g
-
-  infix 4 _≃_
-
-  ≃-isEquivalence : IsEquivalence _≃_
-  ≃-isEquivalence = let open MonotoneMap.≃ in record
-      { refl = λ {x} → refl {x = F x}
-      ; sym = λ {f g} → sym {x = F f} {y = F g}
-      ; trans = λ {f g h} → trans {i = F f} {j = F g} {k = F h}
-      }
-
-  module ≃ = IsEquivalence ≃-isEquivalence
-
-private
-
-  identity : {c ℓ : Level} (A : MonoidalPreorder c ℓ) → MonoidalMonotone A A
-  identity A = let open MonoidalPreorder A in record
-      { F = Category.id (Preorders _ _)
-      ; ε = refl
-      ; ⊗-homo = λ p₁ p₂ → refl {p₁ ⊗ p₂}
-      }
-
-  compose
-      : {c ℓ : Level}
-        {P Q R : MonoidalPreorder c ℓ}
-      → MonoidalMonotone Q R
-      → MonoidalMonotone P Q
-      → MonoidalMonotone P R
-  compose {R = R} G F = record
-      { F = let open Category (Preorders _ _) in G.F ∘ F.F
-      ; ε = trans G.ε (G.mono F.ε)
-      ; ⊗-homo = λ p₁ p₂ → trans (G.⊗-homo (F.map p₁) (F.map p₂)) (G.mono (F.⊗-homo p₁ p₂))
-      }
-    where
-      module F = MonoidalMonotone F
-      module G = MonoidalMonotone G
-      open MonoidalPreorder R
-
-  compose-resp-≃
-      : {c ℓ : Level}
-        {A B C : MonoidalPreorder c ℓ}
-        {f h : MonoidalMonotone B C}
-        {g i : MonoidalMonotone A B}
-      → f ≃ h
-      → g ≃ i
-      → compose f g ≃ compose h i
-  compose-resp-≃ {C = C} {f = f} {g} {h} {i} = ∘-resp-≈ {f = F f} {F g} {F h} {F i}
-    where
-      open Category (Preorders _ _)
-      open MonoidalMonotone using (F)
-
-MonoidalPreorders : (c ℓ : Level) → Category (suc (c ⊔ ℓ)) (c ⊔ ℓ) (c ⊔ ℓ)
-MonoidalPreorders c ℓ = categoryHelper record
-    { Obj = MonoidalPreorder c ℓ
-    ; _⇒_ = MonoidalMonotone
-    ; _≈_ = _≃_
-    ; 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}
-    }
-  where
-    open MonoidalMonotone using (F)
-- 
cgit v1.2.3