blob: 7475719ae94ede4fc32ad68247350e55d0e2e08f (
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
|
{-# OPTIONS --without-K --safe #-}
module Category.Instance.SymMonPre.Primitive where
import Category.Instance.MonoidalPreorders.Primitive as MP using (_≃_; module ≃)
open import Categories.Category using (Category)
open import Categories.Category.Helper using (categoryHelper)
open import Category.Instance.MonoidalPreorders.Primitive using (MonoidalPreorders)
open import Level using (Level; suc; _⊔_)
open import Preorder.Primitive.Monoidal using (SymmetricMonoidalPreorder; SymmetricMonoidalMonotone)
open import Relation.Binary using (IsEquivalence)
module _ {c₁ c₂ ℓ₁ ℓ₂ : Level} {A : SymmetricMonoidalPreorder c₁ ℓ₁} {B : SymmetricMonoidalPreorder c₂ ℓ₂} where
open SymmetricMonoidalMonotone using () renaming (monoidalMonotone to mM)
-- Pointwise isomorphism of symmetric monoidal monotone maps
_≃_ : (f g : SymmetricMonoidalMonotone A B) → Set (c₁ ⊔ ℓ₂)
f ≃ g = mM f MP.≃ mM g
infix 4 _≃_
≃-isEquivalence : IsEquivalence _≃_
≃-isEquivalence = let open MP.≃ in record
{ refl = λ {x} → refl {x = mM x}
; sym = λ {f g} → sym {x = mM f} {y = mM g}
; trans = λ {f g h} → trans {i = mM f} {j = mM g} {k = mM h}
}
module ≃ = IsEquivalence ≃-isEquivalence
private
identity : {c ℓ : Level} (A : SymmetricMonoidalPreorder c ℓ) → SymmetricMonoidalMonotone A A
identity {c} {ℓ} A = record
{ monoidalMonotone = id {monoidalPreorder}
}
where
open SymmetricMonoidalPreorder A using (monoidalPreorder)
open Category (MonoidalPreorders c ℓ) using (id)
compose
: {c ℓ : Level}
{P Q R : SymmetricMonoidalPreorder c ℓ}
→ SymmetricMonoidalMonotone Q R
→ SymmetricMonoidalMonotone P Q
→ SymmetricMonoidalMonotone P R
compose {c} {ℓ} {R = R} G F = record
{ monoidalMonotone = G.monoidalMonotone ∘ F.monoidalMonotone
}
where
module G = SymmetricMonoidalMonotone G
module F = SymmetricMonoidalMonotone F
open Category (MonoidalPreorders c ℓ) using (_∘_)
compose-resp-≃
: {c ℓ : Level}
{A B C : SymmetricMonoidalPreorder c ℓ}
{f h : SymmetricMonoidalMonotone B C}
{g i : SymmetricMonoidalMonotone A B}
→ f ≃ h
→ g ≃ i
→ compose f g ≃ compose h i
compose-resp-≃ {C = C} {f = f} {g} {h} {i} = ∘-resp-≈ {f = mM f} {mM g} {mM h} {mM i}
where
open Category (MonoidalPreorders _ _)
open SymmetricMonoidalMonotone using () renaming (monoidalMonotone to mM)
-- The category of symmetric monoidal preorders
SymMonPre : (c ℓ : Level) → Category (suc (c ⊔ ℓ)) (c ⊔ ℓ) (c ⊔ ℓ)
SymMonPre c ℓ = categoryHelper record
{ Obj = SymmetricMonoidalPreorder c ℓ
; _⇒_ = SymmetricMonoidalMonotone
; _≈_ = _≃_
; id = λ {A} → identity A
; _∘_ = compose
; assoc = λ {f = f} {g h} → ≃.refl {x = compose (compose h g) f}
; identityˡ = λ {f = f} → ≃.refl {x = f}
; identityʳ = λ {f = f} → ≃.refl {x = f}
; equiv = ≃-isEquivalence
; ∘-resp-≈ = λ {f = f} {g h i} → compose-resp-≃ {f = f} {g} {h} {i}
}
|
