blob: 612e91c56f94e90f5eaa1b7b0716cdefacf8bc95 (
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
|
{-# OPTIONS --without-K --safe #-}
module Functor.Free.Instance.MonoidalPreorder.Strong where
import Categories.Category.Monoidal.Utilities as ⊗-Util
import Functor.Free.Instance.Preorder as Preorder
open import Categories.Category using (Category)
open import Categories.Category.Instance.Monoidals using (StrongMonoidals)
open import Categories.Category.Monoidal using (MonoidalCategory)
open import Categories.Functor using (Functor)
open import Categories.Functor.Monoidal using (StrongMonoidalFunctor)
open import Categories.Functor.Monoidal.Properties using (∘-StrongMonoidal)
open import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal using (module Strong)
open import Category.Instance.Preorder.Primitive.Monoidals.Strong using (_≃_; module ≃) renaming (Monoidals to Monoidalsₚ)
open import Data.Product using (_,_)
open import Level using (Level)
open import Preorder.Primitive using (module Isomorphism)
open import Preorder.Primitive.MonotoneMap using (MonotoneMap)
open import Preorder.Primitive.Monoidal using (MonoidalPreorder)
open import Preorder.Primitive.MonotoneMap.Monoidal.Strong using (MonoidalMonotone)
open Strong using (MonoidalNaturalIsomorphism)
-- The free monoidal preorder of a monoidal category
module _ {o ℓ e : Level} where
monoidalPreorder : MonoidalCategory o ℓ e → MonoidalPreorder o ℓ
monoidalPreorder C = record
{ U = Preorder.Free.₀ U
; monoidal = record
{ unit = unit
; tensor = Preorder.Free.₁ ⊗
; unitaryˡ = Preorder.Free.F-resp-≈ unitorˡ-naturalIsomorphism
; unitaryʳ = Preorder.Free.F-resp-≈ unitorʳ-naturalIsomorphism
; associative = λ x y z → record
{ from = associator.from {x} {y} {z}
; to = associator.to {x} {y} {z}
}
}
}
where
open MonoidalCategory C
open ⊗-Util monoidal
module _ {A B : MonoidalCategory o ℓ e} where
monoidalMonotone : StrongMonoidalFunctor A B → MonoidalMonotone (monoidalPreorder A) (monoidalPreorder B)
monoidalMonotone F = record
{ F = Preorder.Free.₁ F.F
; ε = record { F.ε }
; ⊗-homo = λ p₁ p₂ → Preorder.Free.F-resp-≈ F.⊗-homo (p₁ , p₂)
}
where
module F = StrongMonoidalFunctor F
open MonoidalNaturalIsomorphism using (U)
pointwiseIsomorphism
: {F G : StrongMonoidalFunctor A B}
→ MonoidalNaturalIsomorphism F G
→ monoidalMonotone F ≃ monoidalMonotone G
pointwiseIsomorphism F≃G = Preorder.Free.F-resp-≈ (U F≃G)
Free : {o ℓ e : Level} → Functor (StrongMonoidals o ℓ e) (Monoidalsₚ o ℓ)
Free = record
{ F₀ = monoidalPreorder
; F₁ = monoidalMonotone
; identity = λ {A} → ≃.refl {A = monoidalPreorder A} {x = id}
; homomorphism = λ {f = f} {h} → ≃.refl {x = monoidalMonotone (∘-StrongMonoidal h f)}
; F-resp-≈ = pointwiseIsomorphism
}
where
open Category (Monoidalsₚ _ _) using (id)
module Free {o ℓ e} = Functor (Free {o} {ℓ} {e})
|
