blob: 86111deddc94f92aeb16e2587352b849d023c249 (
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
|
{-# OPTIONS --without-K --safe #-}
open import Level using (Level; _⊔_; suc)
module SplitIdempotents.CMonoids {c ℓ : Level} where
import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
import SplitIdempotents.Monoids as SIM
open import Category.Instance.Setoids.SymmetricMonoidal {c} {ℓ} using (Setoids-×; ×-symmetric′)
open import Categories.Category using (Category)
open import Categories.Category.Instance.Setoids using (Setoids)
open import Categories.Category.Monoidal.Symmetric using (Symmetric)
open import Categories.Object.Monoid Setoids-×.monoidal using (Monoid)
open import Category.Construction.CMonoids Setoids-×.symmetric using (CMonoids)
open import Data.Product using (_,_)
open import Data.Setoid using (∣_∣)
open import Function using (_⟶ₛ_; _⟨$⟩_)
open import Function.Construct.Setoid using (_∙_)
open import Morphism.SplitIdempotent CMonoids using (IsSplitIdempotent)
open import Object.Monoid.Commutative Setoids-×.symmetric using (CommutativeMonoid; CommutativeMonoid⇒)
open import Relation.Binary using (Setoid)
open Category CMonoids using (_∘_; _≈_)
open Symmetric Setoids-×.symmetric using (_⊗₀_; unit; _⊗₁_)
module _ {M : CommutativeMonoid} (F : CommutativeMonoid⇒ M M) where
private
module M = CommutativeMonoid M
module F = CommutativeMonoid⇒ F
module MQ = Monoid (SIM.Q F.monoid⇒)
X : Setoid c ℓ
X = MQ.Carrier
private
module X = Setoid X
module S = Setoid M.Carrier
open ≈-Reasoning M.Carrier
opaque
unfolding ×-symmetric′ SIM.μ
comm
: {x : ∣ MQ.Carrier ⊗₀ MQ.Carrier ∣}
→ (MQ.μ ⟨$⟩ x)
X.≈ (MQ.μ ∙ Setoids-×.braiding.⇒.η (X , X) ⟨$⟩ x)
comm {x , y} = begin
F.arr ⟨$⟩ (MQ.μ ⟨$⟩ (x , y)) ≈⟨ F.preserves-μ ⟩
MQ.μ ⟨$⟩ (F.arr ⟨$⟩ x , F.arr ⟨$⟩ y) ≈⟨ M.commutative ⟩
MQ.μ ⟨$⟩ (F.arr ⟨$⟩ y , F.arr ⟨$⟩ x) ≈⟨ F.preserves-μ ⟨
F.arr ⟨$⟩ (MQ.μ ⟨$⟩ (y , x)) ∎
Q : CommutativeMonoid
Q = record
{ Carrier = X
; isCommutativeMonoid = record
{ isMonoid = MQ.isMonoid
; commutative = comm
}
}
M⇒Q : CommutativeMonoid⇒ M Q
M⇒Q = record
{ monoid⇒ = SIM.M⇒Q F.monoid⇒
}
Q⇒M : CommutativeMonoid⇒ Q M
Q⇒M = record
{ monoid⇒ = SIM.Q⇒M F.monoid⇒
}
module _ (idem : F ∘ F ≈ F) where
split : IsSplitIdempotent F
split = record
{ B = Q
; r = M⇒Q
; s = Q⇒M
; s∘r = S.refl
; r∘s = idem
}
|
