blob: 6bdeb3fbbf51346591a82bc90dfcc05dd2bfaf65 (
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
|
{-# OPTIONS --without-K --safe #-}
module Category.Instance.MonoidalPreorders where
import Category.Instance.Preorders as MonotoneMap using (_≗_; module ≗)
import Relation.Binary.Morphism.Construct.Composition as Comp
import Relation.Binary.Morphism.Construct.Identity as Id
open import Categories.Category using (Category)
open import Categories.Category.Helper using (categoryHelper)
open import Level using (Level; suc; _⊔_)
open import Preorder.Monoidal using (MonoidalPreorder; MonoidalMonotone)
open import Relation.Binary using (IsEquivalence)
private
identity : {c ℓ e : Level} (A : MonoidalPreorder c ℓ e) → MonoidalMonotone A A
identity A = let open MonoidalPreorder A in record
{ F = Id.preorderHomomorphism U
; ε = refl {unit}
; ⊗-homo = λ p₁ p₂ → refl {p₁ ⊗ p₂}
}
compose
: {c ℓ e : Level}
{P Q R : MonoidalPreorder c ℓ e}
→ MonoidalMonotone Q R
→ MonoidalMonotone P Q
→ MonoidalMonotone P R
compose {R = R} G F = record
{ F = Comp.preorderHomomorphism F.F G.F
; ε = trans G.ε (G.mono F.ε)
; ⊗-homo = λ p₁ p₂ → trans (G.⊗-homo F.⟦ p₁ ⟧ F.⟦ p₂ ⟧) (G.mono (F.⊗-homo p₁ p₂))
}
where
module F = MonoidalMonotone F
module G = MonoidalMonotone G
open MonoidalPreorder R
module _ {c₁ c₂ ℓ₁ ℓ₂ e₁ e₂ : Level} {A : MonoidalPreorder c₁ ℓ₁ e₁} {B : MonoidalPreorder c₂ ℓ₂ e₂} where
-- Pointwise equality of monoidal monotone maps
open MonoidalMonotone using (F)
_≗_ : (f g : MonoidalMonotone A B) → Set (c₁ ⊔ ℓ₂)
f ≗ g = F f MonotoneMap.≗ F g
infix 4 _≗_
≗-isEquivalence : IsEquivalence _≗_
≗-isEquivalence = let open MonotoneMap.≗ in record
{ refl = λ {x} → refl {x = F x}
; sym = λ {f g} → sym {x = F f} {y = F g}
; trans = λ {f g h} → trans {i = F f} {j = F g} {k = F h}
}
module ≗ = IsEquivalence ≗-isEquivalence
MonoidalPreorders : (c ℓ e : Level) → Category (suc (c ⊔ ℓ ⊔ e)) (c ⊔ ℓ ⊔ e) (c ⊔ ℓ)
MonoidalPreorders c ℓ e = categoryHelper record
{ Obj = MonoidalPreorder c ℓ e
; _⇒_ = MonoidalMonotone
; _≈_ = _≗_
; id = λ {A} → identity A
; _∘_ = λ {A B C} f g → compose f g
; assoc = λ {_ _ _ D _ _ _ _} → Eq.refl D
; identityˡ = λ {_ B _ _} → Eq.refl B
; identityʳ = λ {_ B _ _} → Eq.refl B
; equiv = ≗-isEquivalence
; ∘-resp-≈ = λ {_ _ C _ h} f≈h g≈i → Eq.trans C f≈h (cong h g≈i)
}
where
open MonoidalMonotone using (F; cong)
open MonoidalPreorder using (U; refl; module Eq)
|
