blob: 20cc6e72e2114e5ce0456aaef652ed15cd8e469b (
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
|
{-# OPTIONS --without-K --safe #-}
open import Level using (Level)
module Functor.Free.Instance.InducedMonoid {c ℓ : Level} where
-- The induced monoid of a monoidal preorder
open import Category.Instance.Setoids.SymmetricMonoidal {c} {ℓ} using (Setoids-×; ×-monoidal′)
open import Categories.Object.Monoid Setoids-×.monoidal using (Monoid; Monoid⇒)
open import Categories.Category.Construction.Monoids Setoids-×.monoidal using (Monoids)
open import Categories.Functor using (Functor)
open import Category.Instance.Preorder.Primitive.Monoidals.Strong using (Monoidals)
open import Category.Cartesian.Instance.Preorders.Primitive using (Preorders-CC; ⊤ₚ)
open import Preorder.Primitive using (Preorder)
open import Preorder.Primitive.Monoidal using (MonoidalPreorder; _×ₚ_)
open import Preorder.Primitive.MonotoneMap.Monoidal.Strong using (MonoidalMonotone)
open import Preorder.Primitive using (module Isomorphism)
open import Data.Product using (_,_)
open import Functor.Cartesian.Instance.InducedSetoid using () renaming (module InducedSetoid to IS)
open import Function using (Func; _⟨$⟩_)
open import Function.Construct.Setoid using (_∙_)
open import Data.Setoid.Unit using (⊤ₛ)
open import Data.Setoid using (∣_∣)
open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
open import Function.Construct.Constant using () renaming (function to Const)
open import Function.Construct.Identity using () renaming (function to Id)
open import Relation.Binary using (Setoid)
open Setoids-× using (_⊗₀_; _⊗₁_; module unitorˡ; module unitorʳ; module associator; _≈_)
module _ (P : MonoidalPreorder c ℓ) where
open MonoidalPreorder P
open Isomorphism U using (module ≅; _≅_)
M : Setoid c ℓ
M = IS.₀ U
opaque
unfolding ×-monoidal′
μ : Func (M ⊗₀ M) M
μ = IS.₁ tensor ∙ IS.×-iso.to U U
η : Func Setoids-×.unit M
η = Const Setoids-×.unit M unit
opaque
unfolding μ
assoc : μ ∙ μ ⊗₁ Id M ≈ μ ∙ Id M ⊗₁ μ ∙ associator.from
assoc {(x , y) , z} = associative x y z
identityˡ : unitorˡ.from ≈ μ ∙ η ⊗₁ Id M
identityˡ {_ , x} = ≅.sym (unitaryˡ x)
identityʳ : unitorʳ.from ≈ μ ∙ Id M ⊗₁ η
identityʳ {x , _} = ≅.sym (unitaryʳ x)
≅-monoid : Monoid
≅-monoid = record
{ Carrier = M
; isMonoid = record
{ μ = μ
; η = Const Setoids-×.unit M unit
; assoc = assoc
; identityˡ = identityˡ
; identityʳ = identityʳ
}
}
module _ {A B : MonoidalPreorder c ℓ} (f : MonoidalMonotone A B) where
private
module A = MonoidalPreorder A
module B = MonoidalPreorder B
open Isomorphism B.U using (_≅_; module ≅)
open MonoidalMonotone f
opaque
unfolding μ
preserves-μ
: {x : ∣ IS.₀ A.U ⊗₀ IS.₀ A.U ∣}
→ map (μ A ⟨$⟩ x)
≅ μ B ⟨$⟩ (IS.₁ F ⊗₁ IS.₁ F ⟨$⟩ x)
preserves-μ {x , y} = ≅.sym (⊗-homo x y)
monoid⇒ : Monoid⇒ (≅-monoid A) (≅-monoid B)
monoid⇒ = record
{ arr = IS.₁ F
; preserves-μ = preserves-μ
; preserves-η = ≅.sym ε
}
InducedMonoid : Functor (Monoidals c ℓ) Monoids
InducedMonoid = record
{ F₀ = ≅-monoid
; F₁ = monoid⇒
; identity = λ {A} {x} → ≅.refl (U A)
; homomorphism = λ {Z = Z} → ≅.refl (U Z)
; F-resp-≈ = λ f≃g {x} → f≃g x
}
where
open MonoidalPreorder using (U)
open Isomorphism using (module ≅)
module InducedMonoid = Functor InducedMonoid
|
