1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
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
|
