diff options
| author | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-01-04 16:15:11 -0600 |
|---|---|---|
| committer | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-01-04 16:15:11 -0600 |
| commit | 3386254cb6f5fc36c5cb18b7240edde3210a376c (patch) | |
| tree | cfe3eb553afab97c12634e62931f9fa1d378397b /Preorder | |
| parent | 3d7c5574124d3384ff942489feaa093618c309b9 (diff) | |
Add category of symmetric monoidal preorders
Diffstat (limited to 'Preorder')
| -rw-r--r-- | Preorder/Monoidal.agda | 23 |
1 files changed, 21 insertions, 2 deletions
diff --git a/Preorder/Monoidal.agda b/Preorder/Monoidal.agda index 02c6d88..34763c7 100644 --- a/Preorder/Monoidal.agda +++ b/Preorder/Monoidal.agda @@ -67,6 +67,9 @@ record SymmetricMonoidalPreorder (c ℓ e : Level) : Set (suc (c ⊔ ℓ ⊔ e)) monoidal : Monoidal U symmetric : Symmetric monoidal + monoidalPreorder : MonoidalPreorder c ℓ e + monoidalPreorder = record { monoidal = monoidal } + open Preorder U public open Monoidal monoidal public open Symmetric symmetric public @@ -77,8 +80,9 @@ record MonoidalMonotone (Q : MonoidalPreorder c₂ ℓ₂ e₂) : Set (c₁ ⊔ c₂ ⊔ ℓ₁ ⊔ ℓ₂ ⊔ e₁ ⊔ e₂) where - module P = MonoidalPreorder P - module Q = MonoidalPreorder Q + private + module P = MonoidalPreorder P + module Q = MonoidalPreorder Q field F : PreorderHomomorphism P.U Q.U @@ -88,3 +92,18 @@ record MonoidalMonotone field ε : Q.unit Q.≲ ⟦ P.unit ⟧ ⊗-homo : (p₁ p₂ : P.Carrier) → ⟦ p₁ ⟧ Q.⊗ ⟦ p₂ ⟧ Q.≲ ⟦ p₁ P.⊗ p₂ ⟧ + +record SymmetricMonoidalMonotone + {c₁ c₂ ℓ₁ ℓ₂ e₁ e₂ : Level} + (P : SymmetricMonoidalPreorder c₁ ℓ₁ e₁) + (Q : SymmetricMonoidalPreorder c₂ ℓ₂ e₂) + : Set (c₁ ⊔ c₂ ⊔ ℓ₁ ⊔ ℓ₂ ⊔ e₁ ⊔ e₂) where + + private + module P = SymmetricMonoidalPreorder P + module Q = SymmetricMonoidalPreorder Q + + field + monoidalMonotone : MonoidalMonotone P.monoidalPreorder Q.monoidalPreorder + + open MonoidalMonotone monoidalMonotone public |