Differentiate lax and strong monoidal monotones

5 files changed, 405 insertions, 0 deletions

diff --git a/Category/Instance/Preorder/Primitive/Monoidals/Lax.agda b/Category/Instance/Preorder/Primitive/Monoidals/Lax.agda
new file mode 100644
index 0000000..cbd4015
--- /dev/null
+++ b/Category/Instance/Preorder/Primitive/Monoidals/Lax.agda
@@ -0,0 +1,87 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Category.Instance.Preorder.Primitive.Monoidals.Lax 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.Preorder.Primitive.Preorders using (Preorders)
+open import Level using (Level; suc; _⊔_)
+open import Preorder.Primitive.Monoidal using (MonoidalPreorder)
+open import Preorder.Primitive.MonotoneMap.Monoidal.Lax using (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)
+
+Monoidals : (c ℓ : Level) → Category (suc (c ⊔ ℓ)) (c ⊔ ℓ) (c ⊔ ℓ)
+Monoidals 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)
diff --git a/Category/Instance/Preorder/Primitive/Monoidals/Strong.agda b/Category/Instance/Preorder/Primitive/Monoidals/Strong.agda
new file mode 100644
index 0000000..470db1c
--- /dev/null
+++ b/Category/Instance/Preorder/Primitive/Monoidals/Strong.agda
@@ -0,0 +1,92 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Category.Instance.Preorder.Primitive.Monoidals.Strong 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.Preorder.Primitive.Preorders using (Preorders)
+open import Level using (Level; suc; _⊔_)
+open import Preorder.Primitive using (module Isomorphism)
+open import Preorder.Primitive.Monoidal using (MonoidalPreorder)
+open import Preorder.Primitive.MonotoneMap.Monoidal.Strong using (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 = record
+      { F = Category.id (Preorders _ _)
+      ; ε = ≅.refl
+      ; ⊗-homo = λ p₁ p₂ → ≅.refl {p₁ ⊗ p₂}
+      }
+    where
+      open MonoidalPreorder A
+      open Isomorphism U using (module ≅)
+
+  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.map-resp-≅ F.ε)
+      ; ⊗-homo = λ p₁ p₂ → ≅.trans (G.⊗-homo (F.map p₁) (F.map p₂)) (G.map-resp-≅ (F.⊗-homo p₁ p₂))
+      }
+    where
+      module F = MonoidalMonotone F
+      module G = MonoidalMonotone G
+      open MonoidalPreorder R
+      open Isomorphism U using (module ≅)
+
+  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)
+
+Monoidals : (c ℓ : Level) → Category (suc (c ⊔ ℓ)) (c ⊔ ℓ) (c ⊔ ℓ)
+Monoidals 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)
diff --git a/Category/Instance/Preorder/Primitive/Monoidals/Symmetric/Lax.agda b/Category/Instance/Preorder/Primitive/Monoidals/Symmetric/Lax.agda
new file mode 100644
index 0000000..c15ff29
--- /dev/null
+++ b/Category/Instance/Preorder/Primitive/Monoidals/Symmetric/Lax.agda
@@ -0,0 +1,84 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Category.Instance.Preorder.Primitive.Monoidals.Symmetric.Lax where
+
+import Category.Instance.Preorder.Primitive.Monoidals.Lax as MP using (_≃_; module ≃)
+
+open import Categories.Category using (Category)
+open import Categories.Category.Helper using (categoryHelper)
+open import Category.Instance.Preorder.Primitive.Monoidals.Lax using (Monoidals)
+open import Level using (Level; suc; _⊔_)
+open import Preorder.Primitive.Monoidal using (SymmetricMonoidalPreorder)
+open import Preorder.Primitive.MonotoneMap.Monoidal.Lax using (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 (Monoidals 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 (Monoidals 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 (Monoidals _ _)
+      open SymmetricMonoidalMonotone using () renaming (monoidalMonotone to mM)
+
+-- The category of symmetric monoidal preorders and lax symmetric monoidal monotone
+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}
+    }
diff --git a/Category/Instance/Preorder/Primitive/Monoidals/Symmetric/Strong.agda b/Category/Instance/Preorder/Primitive/Monoidals/Symmetric/Strong.agda
new file mode 100644
index 0000000..b584ed7
--- /dev/null
+++ b/Category/Instance/Preorder/Primitive/Monoidals/Symmetric/Strong.agda
@@ -0,0 +1,84 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Category.Instance.Preorder.Primitive.Monoidals.Symmetric.Strong where
+
+import Category.Instance.Preorder.Primitive.Monoidals.Strong as MP using (_≃_; module ≃)
+
+open import Categories.Category using (Category)
+open import Categories.Category.Helper using (categoryHelper)
+open import Category.Instance.Preorder.Primitive.Monoidals.Strong using (Monoidals)
+open import Level using (Level; suc; _⊔_)
+open import Preorder.Primitive.Monoidal using (SymmetricMonoidalPreorder)
+open import Preorder.Primitive.MonotoneMap.Monoidal.Strong using (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 (Monoidals 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 (Monoidals 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 (Monoidals _ _)
+      open SymmetricMonoidalMonotone using () renaming (monoidalMonotone to mM)
+
+-- The category of symmetric monoidal preorders and strong symmetric monoidal monotone
+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}
+    }
diff --git a/Category/Instance/Preorder/Primitive/Preorders.agda b/Category/Instance/Preorder/Primitive/Preorders.agda
new file mode 100644
index 0000000..9832376
--- /dev/null
+++ b/Category/Instance/Preorder/Primitive/Preorders.agda
@@ -0,0 +1,58 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Category.Instance.Preorder.Primitive.Preorders where
+
+open import Categories.Category using (Category)
+open import Categories.Category.Helper using (categoryHelper)
+open import Function using (id; _∘_)
+open import Level using (Level; _⊔_; suc)
+open import Preorder.Primitive using (Preorder; module Isomorphism)
+open import Preorder.Primitive.MonotoneMap using (MonotoneMap; _≃_; ≃-isEquivalence; module ≃)
+
+-- The category of primitive preorders and monotone maps
+
+private
+
+  module _ {c ℓ : Level} where
+
+    identity : {A : Preorder c ℓ} → MonotoneMap A A
+    identity = record
+        { map = id
+        ; mono = id
+        }
+
+    compose : {A B C : Preorder c ℓ} → MonotoneMap B C → MonotoneMap A B → MonotoneMap A C
+    compose f g = record
+        { map = f.map ∘ g.map
+        ; mono = f.mono ∘ g.mono
+        }
+      where
+        module f = MonotoneMap f
+        module g = MonotoneMap g
+
+    compose-resp-≃
+        : {A B C : Preorder c ℓ}
+          {f h : MonotoneMap B C}
+          {g i : MonotoneMap A B}
+        → f ≃ h
+        → g ≃ i
+        → compose f g ≃ compose h i
+    compose-resp-≃ {C = C} {h = h} {g} f≃h g≃i x = ≅.trans (f≃h (map g x)) (map-resp-≅ h (g≃i x))
+      where
+        open MonotoneMap using (map; mono; map-resp-≅)
+        open Preorder C
+        open Isomorphism C
+
+Preorders : (c ℓ : Level) → Category (suc (c ⊔ ℓ)) (c ⊔ ℓ) (c ⊔ ℓ)
+Preorders c ℓ = categoryHelper record
+    { Obj = Preorder c ℓ
+    ; _⇒_ = MonotoneMap
+    ; _≈_ = _≃_
+    ; id = identity
+    ; _∘_ = 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}
+    }