blob: df48063f75ea756ce779b20a661e462d562bafa6 (
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
|
{-# OPTIONS --without-K --safe #-}
open import Categories.Category.Core using (Category)
open import Categories.Category.Monoidal.Core using (Monoidal)
open import Level using (Level; _⊔_)
module Category.Construction.Monoids.Properties
{o ℓ e : Level}
{𝒞 : Category o ℓ e}
(monoidal : Monoidal 𝒞)
where
import Categories.Category.Monoidal.Reasoning monoidal as ⊗-Reasoning
import Categories.Morphism.Reasoning 𝒞 as ⇒-Reasoning
open import Categories.Category using (_[_,_])
open import Categories.Category.Construction.Monoids monoidal using (Monoids)
open import Categories.Category.Monoidal.Utilities monoidal using (module Shorthands; _⊗ᵢ_)
open import Categories.Morphism using (_≅_)
open import Categories.Morphism.Notation using (_[_≅_])
open import Categories.Object.Monoid monoidal using (Monoid)
open import Data.Product using (Σ-syntax; _,_)
module 𝒞 = Category 𝒞
open Monoid using () renaming (Carrier to ∣_∣)
transport-by-iso
: {X : 𝒞.Obj}
→ (M : Monoid)
→ 𝒞 [ ∣ M ∣ ≅ X ]
→ Σ[ Xₘ ∈ Monoid ] Monoids [ M ≅ Xₘ ]
transport-by-iso {X} M ∣M∣≅X = Xₘ , M≅Xₘ
where
open _≅_ ∣M∣≅X
open Monoid M
open 𝒞 using (_∘_; id; _≈_; module Equiv)
open Monoidal monoidal
using (_⊗₀_; _⊗₁_; assoc-commute-from; unitorˡ-commute-from; unitorʳ-commute-from)
open Shorthands
open ⊗-Reasoning
open ⇒-Reasoning
as
: (from ∘ μ ∘ to ⊗₁ to)
∘ (from ∘ μ ∘ to ⊗₁ to) ⊗₁ id
≈ (from ∘ μ ∘ to ⊗₁ to)
∘ id ⊗₁ (from ∘ μ ∘ to ⊗₁ to)
∘ α⇒
as = extendˡ (begin
(μ ∘ to ⊗₁ to) ∘ (from ∘ μ ∘ to ⊗₁ to) ⊗₁ id ≈⟨ pullʳ merge₁ʳ ⟩
μ ∘ (to ∘ from ∘ μ ∘ to ⊗₁ to) ⊗₁ to ≈⟨ refl⟩∘⟨ cancelˡ isoˡ ⟩⊗⟨refl ⟩
μ ∘ (μ ∘ to ⊗₁ to) ⊗₁ to ≈⟨ refl⟩∘⟨ split₁ˡ ⟩
μ ∘ μ ⊗₁ id ∘ (to ⊗₁ to) ⊗₁ to ≈⟨ extendʳ assoc ⟩
μ ∘ (id ⊗₁ μ ∘ α⇒) ∘ (to ⊗₁ to) ⊗₁ to ≈⟨ pushʳ (pullʳ assoc-commute-from) ⟩
(μ ∘ id ⊗₁ μ) ∘ to ⊗₁ (to ⊗₁ to) ∘ α⇒ ≈⟨ extendˡ (pullˡ merge₂ˡ) ⟩
(μ ∘ to ⊗₁ (μ ∘ to ⊗₁ to)) ∘ α⇒ ≈⟨ (refl⟩∘⟨ refl⟩⊗⟨ insertˡ isoˡ) ⟩∘⟨refl ⟩
(μ ∘ to ⊗₁ (to ∘ from ∘ μ ∘ to ⊗₁ to)) ∘ α⇒ ≈⟨ pushˡ (pushʳ split₂ʳ) ⟩
(μ ∘ to ⊗₁ to) ∘ id ⊗₁ (from ∘ μ ∘ to ⊗₁ to) ∘ α⇒ ∎)
idˡ : λ⇒ ≈ (from ∘ μ ∘ to ⊗₁ to) ∘ (from ∘ η) ⊗₁ id
idˡ = begin
λ⇒ ≈⟨ insertˡ isoʳ ⟩
from ∘ to ∘ λ⇒ ≈⟨ refl⟩∘⟨ unitorˡ-commute-from ⟨
from ∘ λ⇒ ∘ id ⊗₁ to ≈⟨ refl⟩∘⟨ pushˡ identityˡ ⟩
from ∘ μ ∘ η ⊗₁ id ∘ id ⊗₁ to ≈⟨ refl⟩∘⟨ refl⟩∘⟨ serialize₁₂ ⟨
from ∘ μ ∘ η ⊗₁ to ≈⟨ refl⟩∘⟨ refl⟩∘⟨ insertˡ isoˡ ⟩⊗⟨refl ⟩
from ∘ μ ∘ (to ∘ from ∘ η) ⊗₁ to ≈⟨ pushʳ (pushʳ split₁ʳ) ⟩
(from ∘ μ ∘ to ⊗₁ to) ∘ (from ∘ η) ⊗₁ id ∎
idʳ : ρ⇒ ≈ (from ∘ μ ∘ to ⊗₁ to) ∘ id ⊗₁ (from ∘ η)
idʳ = begin
ρ⇒ ≈⟨ insertˡ isoʳ ⟩
from ∘ to ∘ ρ⇒ ≈⟨ refl⟩∘⟨ unitorʳ-commute-from ⟨
from ∘ ρ⇒ ∘ to ⊗₁ id ≈⟨ refl⟩∘⟨ pushˡ identityʳ ⟩
from ∘ μ ∘ id ⊗₁ η ∘ to ⊗₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ serialize₂₁ ⟨
from ∘ μ ∘ to ⊗₁ η ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ insertˡ isoˡ ⟩
from ∘ μ ∘ to ⊗₁ (to ∘ from ∘ η) ≈⟨ pushʳ (pushʳ split₂ʳ) ⟩
(from ∘ μ ∘ to ⊗₁ to) ∘ id ⊗₁ (from ∘ η) ∎
Xₘ : Monoid
Xₘ = record
{ Carrier = X
; isMonoid = record
{ μ = from ∘ μ ∘ to ⊗₁ to
; η = from ∘ η
; assoc = as
; identityˡ = idˡ
; identityʳ = idʳ
}
}
M⇒Xₘ : Monoids [ M , Xₘ ]
M⇒Xₘ = record
{ arr = from
; preserves-μ = pushʳ (insertʳ (_≅_.isoˡ (∣M∣≅X ⊗ᵢ ∣M∣≅X)))
; preserves-η = Equiv.refl
}
Xₘ⇒M : Monoids [ Xₘ , M ]
Xₘ⇒M = record
{ arr = to
; preserves-μ = cancelˡ isoˡ
; preserves-η = cancelˡ isoˡ
}
M≅Xₘ : Monoids [ M ≅ Xₘ ]
M≅Xₘ = record
{ from = M⇒Xₘ
; to = Xₘ⇒M
; iso = record
{ isoˡ = isoˡ
; isoʳ = isoʳ
}
}
|
