Add (weak) monoidal and symmetric monoidal preorders

1 files changed, 58 insertions, 0 deletions

diff --git a/Preorder/Monoidal.agda b/Preorder/Monoidal.agda
new file mode 100644
index 0000000..2eb22ae
--- /dev/null
+++ b/Preorder/Monoidal.agda
@@ -0,0 +1,58 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Preorder.Monoidal where
+
+open import Level using (Level; _⊔_; suc)
+open import Relation.Binary.Bundles using (Preorder)
+open import Relation.Binary.Morphism using (PreorderHomomorphism)
+open import Data.Product using (_,_)
+open import Data.Product.Relation.Binary.Pointwise.NonDependent using (×-preorder)
+
+private
+
+  _×ₚ_
+      : {c₁ c₂ ℓ₁ ℓ₂ e₁ e₂ : Level}
+      → Preorder c₁ ℓ₁ e₁
+      → Preorder c₂ ℓ₂ e₂
+      → Preorder (c₁ ⊔ c₂) (ℓ₁ ⊔ ℓ₂) (e₁ ⊔ e₂)
+  _×ₚ_ P Q = ×-preorder P Q
+
+  infixr 2 _×ₚ_
+
+record Monoidal {c ℓ e : Level} (P : Preorder c ℓ e) : Set (c ⊔ ℓ ⊔ e) where
+
+  open Preorder P
+
+  field
+    ⊗ : PreorderHomomorphism (P ×ₚ P) P
+    unit : Carrier
+
+  open PreorderHomomorphism ⊗
+
+  field
+    unitaryˡ-≲ : (x : Carrier) → ⟦ unit , x ⟧ ≲ x
+    unitaryˡ-≳ : (x : Carrier) → x ≲ ⟦ unit , x ⟧
+    unitaryʳ-≲ : (x : Carrier) → ⟦ x , unit ⟧ ≲ x
+    unitaryʳ-≳ : (x : Carrier) → x ≲ ⟦ x , unit ⟧
+    associative-≲ : (x y z : Carrier) → ⟦ ⟦ x , y ⟧ , z ⟧ ≲ ⟦ x , ⟦ y , z ⟧ ⟧
+    associative-≳ : (x y z : Carrier) → ⟦ x , ⟦ y , z ⟧ ⟧ ≲ ⟦ ⟦ x , y ⟧ , z ⟧
+
+record Symmetric {c ℓ e : Level} {P : Preorder c ℓ e} (M : Monoidal P) : Set (c ⊔ e) where
+
+  open Monoidal M
+  open Preorder P
+  open PreorderHomomorphism ⊗
+
+  field
+    symmetric : (x y : Carrier) → ⟦ x , y ⟧ ≲ ⟦ y , x ⟧
+
+record MonoidalPreorder (c ℓ e : Level) : Set (suc (c ⊔ ℓ ⊔ e)) where
+  field
+    U : Preorder c ℓ e
+    monoidal : Monoidal U
+
+record SymmetricMonoidalPreorder (c ℓ e : Level) : Set (suc (c ⊔ ℓ ⊔ e)) where
+  field
+    U : Preorder c ℓ e
+    monoidal : Monoidal U
+    symmetric : Symmetric monoidal