blob: b000d32e9668279b7fe38f5364833ac668bd94f5 (
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
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
|
{-# OPTIONS --without-K --safe #-}
module Preorder.Primitive.Monoidal where
open import Level using (Level; _⊔_; suc)
open import Preorder.Primitive using (Preorder; module Isomorphism)
open import Preorder.Primitive.MonotoneMap using (MonotoneMap)
open import Data.Product using (_×_; _,_)
open import Data.Product.Relation.Binary.Pointwise.NonDependent using (Pointwise; ×-refl; ×-transitive)
private
_×ₚ_
: {c₁ c₂ ℓ₁ ℓ₂ : Level}
→ Preorder c₁ ℓ₁
→ Preorder c₂ ℓ₂
→ Preorder (c₁ ⊔ c₂) (ℓ₁ ⊔ ℓ₂)
_×ₚ_ P Q = record
{ Carrier = P.Carrier × Q.Carrier
; _≲_ = Pointwise P._≲_ Q._≲_
; refl = ×-refl {R = P._≲_} {S = Q._≲_} P.refl Q.refl
; trans = ×-transitive {R = P._≲_} {S = Q._≲_} P.trans Q.trans
}
where
module P = Preorder P
module Q = Preorder Q
infixr 2 _×ₚ_
record Monoidal {c ℓ : Level} (P : Preorder c ℓ) : Set (c ⊔ ℓ) where
open Preorder P
open Isomorphism P
field
unit : Carrier
tensor : MonotoneMap (P ×ₚ P) P
open MonotoneMap tensor using (map)
_⊗_ : Carrier → Carrier → Carrier
_⊗_ x y = map (x , y)
infixr 10 _⊗_
field
unitaryˡ : (x : Carrier) → unit ⊗ x ≅ x
unitaryʳ : (x : Carrier) → x ⊗ unit ≅ x
associative : (x y z : Carrier) → (x ⊗ y) ⊗ z ≅ x ⊗ (y ⊗ z)
record Symmetric {c ℓ : Level} {P : Preorder c ℓ} (M : Monoidal P) : Set (c ⊔ ℓ) where
open Monoidal M
open Preorder P
field
symmetric : (x y : Carrier) → x ⊗ y ≲ y ⊗ x
record MonoidalPreorder (c ℓ : Level) : Set (suc (c ⊔ ℓ)) where
field
U : Preorder c ℓ
monoidal : Monoidal U
open Preorder U public
open Monoidal monoidal public
record SymmetricMonoidalPreorder (c ℓ : Level) : Set (suc (c ⊔ ℓ)) where
field
U : Preorder c ℓ
monoidal : Monoidal U
symmetric : Symmetric monoidal
monoidalPreorder : MonoidalPreorder c ℓ
monoidalPreorder = record { monoidal = monoidal }
open Preorder U public
open Monoidal monoidal public
open Symmetric symmetric public
record MonoidalMonotone
{c₁ c₂ ℓ₁ ℓ₂ : Level}
(P : MonoidalPreorder c₁ ℓ₁)
(Q : MonoidalPreorder c₂ ℓ₂)
: Set (c₁ ⊔ c₂ ⊔ ℓ₁ ⊔ ℓ₂) where
private
module P = MonoidalPreorder P
module Q = MonoidalPreorder Q
field
F : MonotoneMap P.U Q.U
open MonotoneMap F public
field
ε : Q.unit Q.≲ map P.unit
⊗-homo : (p₁ p₂ : P.Carrier) → map p₁ Q.⊗ map p₂ Q.≲ map (p₁ P.⊗ p₂)
record SymmetricMonoidalMonotone
{c₁ c₂ ℓ₁ ℓ₂ : Level}
(P : SymmetricMonoidalPreorder c₁ ℓ₁)
(Q : SymmetricMonoidalPreorder c₂ ℓ₂)
: Set (c₁ ⊔ c₂ ⊔ ℓ₁ ⊔ ℓ₂) where
private
module P = SymmetricMonoidalPreorder P
module Q = SymmetricMonoidalPreorder Q
field
monoidalMonotone : MonoidalMonotone P.monoidalPreorder Q.monoidalPreorder
open MonoidalMonotone monoidalMonotone public
|
