blob: 02c6d8897cd97d33ff445d81e19394f35255a31e (
plain)
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
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
|
{-# 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
unit : Carrier
tensor : PreorderHomomorphism (P ×ₚ P) P
open PreorderHomomorphism tensor using (⟦_⟧)
_⊗_ : Carrier → Carrier → Carrier
_⊗_ x y = ⟦ x , y ⟧
infixr 10 _⊗_
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 tensor
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
open Preorder U public
open Monoidal monoidal public
record SymmetricMonoidalPreorder (c ℓ e : Level) : Set (suc (c ⊔ ℓ ⊔ e)) where
field
U : Preorder c ℓ e
monoidal : Monoidal U
symmetric : Symmetric monoidal
open Preorder U public
open Monoidal monoidal public
open Symmetric symmetric public
record MonoidalMonotone
{c₁ c₂ ℓ₁ ℓ₂ e₁ e₂ : Level}
(P : MonoidalPreorder c₁ ℓ₁ e₁)
(Q : MonoidalPreorder c₂ ℓ₂ e₂)
: Set (c₁ ⊔ c₂ ⊔ ℓ₁ ⊔ ℓ₂ ⊔ e₁ ⊔ e₂) where
module P = MonoidalPreorder P
module Q = MonoidalPreorder Q
field
F : PreorderHomomorphism P.U Q.U
open PreorderHomomorphism F public
field
ε : Q.unit Q.≲ ⟦ P.unit ⟧
⊗-homo : (p₁ p₂ : P.Carrier) → ⟦ p₁ ⟧ Q.⊗ ⟦ p₂ ⟧ Q.≲ ⟦ p₁ P.⊗ p₂ ⟧
|
