Mercurial > hg > Members > kono > Proof > category

annotate em-category.agda @ 471:36d13c7182c1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 06 Mar 2017 17:23:10 +0900
parents ba042c2d3ff5
children a5f2ca67e7c5
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
100
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 -- -- -- -- -- -- -- --
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 -- Monad to Eilenberg-Moore Category
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 -- defines U^T and F^T as a resolution of Monad
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 -- checks Adjointness
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 --
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 -- Shinji KONO <kono@ie.u-ryukyu.ac.jp>
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 -- -- -- -- -- -- -- --
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 -- Monad
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 -- Category A
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 -- A = Category
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 -- Functor T : A → A
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 --T(a) = t(a)
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 --T(f) = tf(f)
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 open import Category -- https://github.com/konn/category-agda
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 open import Level
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 --open import Category.HomReasoning
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 open import HomReasoning
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 open import cat-utility
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 open import Category.Cat
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 module em-category { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ }
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 { T : Functor A A }
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 { η : NTrans A A identityFunctor T }
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 { μ : NTrans A A (T ○ T) T }
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 { M : Monad A T η μ } where
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 --
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30 -- Hom in Eilenberg-Moore Category
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 --
101
0f7086b6a1a6 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 100
diff changeset
32 open Functor
0f7086b6a1a6 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 100
diff changeset
33 open NTrans
114
2032c438b6a6 EM Category constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
34
2032c438b6a6 EM Category constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
35 record IsAlgebra {a : Obj A} { phi : Hom A (FObj T a) a } : Set (c₁ ⊔ c₂ ⊔ ℓ) where
101
0f7086b6a1a6 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 100
diff changeset
36 field
114
2032c438b6a6 EM Category constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
37 identity : A [ A [ phi o TMap η a ] ≈ id1 A a ]
2032c438b6a6 EM Category constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
38 eval : A [ A [ phi o TMap μ a ] ≈ A [ phi o FMap T phi ] ]
100
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39
113
239fa20251ec field version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
40 record EMObj : Set (c₁ ⊔ c₂ ⊔ ℓ) where
239fa20251ec field version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
41 field
465
d3cd28a71b3f clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
42 obj : Obj A
d3cd28a71b3f clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
43 φ : Hom A (FObj T obj) obj
d3cd28a71b3f clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
44 isAlgebra : IsAlgebra {obj} {φ}
108
e763efd30868 on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 107
diff changeset
45 open EMObj
104
53a79dfdcd04 problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
46
465
d3cd28a71b3f clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
47 record EMHom (a : EMObj ) (b : EMObj ) : Set (c₁ ⊔ c₂ ⊔ ℓ) where
100
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
48 field
113
239fa20251ec field version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
49 EMap : Hom A (obj a) (obj b)
114
2032c438b6a6 EM Category constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
50 homomorphism : A [ A [ (φ b) o FMap T EMap ] ≈ A [ EMap o (φ a) ] ]
465
d3cd28a71b3f clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
51 open EMHom
100
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
52
113
239fa20251ec field version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
53 Lemma-EM1 : {x : Obj A} {φ : Hom A (FObj T x) x} (a : EMObj )
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 130
diff changeset
54 → A [ A [ φ o FMap T (id1 A x) ] ≈ A [ (id1 A x) o φ ] ]
108
e763efd30868 on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 107
diff changeset
55 Lemma-EM1 {x} {φ} a = let open ≈-Reasoning (A) in
101
0f7086b6a1a6 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 100
diff changeset
56 begin
0f7086b6a1a6 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 100
diff changeset
57 φ o FMap T (id1 A x)
0f7086b6a1a6 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 100
diff changeset
58 ≈⟨ cdr ( IsFunctor.identity (isFunctor T) ) ⟩
0f7086b6a1a6 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 100
diff changeset
59 φ o (id1 A (FObj T x))
0f7086b6a1a6 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 100
diff changeset
60 ≈⟨ idR ⟩
0f7086b6a1a6 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 100
diff changeset
61 φ
0f7086b6a1a6 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 100
diff changeset
62 ≈⟨ sym idL ⟩
0f7086b6a1a6 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 100
diff changeset
63 (id1 A x) o φ
0f7086b6a1a6 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 100
diff changeset
64 ∎
0f7086b6a1a6 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 100
diff changeset
65
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 130
diff changeset
66 EM-id : { a : EMObj } → EMHom a a
113
239fa20251ec field version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
67 EM-id {a} = record { EMap = id1 A (obj a);
465
d3cd28a71b3f clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
68 homomorphism = Lemma-EM1 {obj a} {φ a} a }
100
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
69
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
70 open import Relation.Binary.Core
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
71
113
239fa20251ec field version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
72 Lemma-EM2 : (a : EMObj )
239fa20251ec field version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
73 (b : EMObj )
239fa20251ec field version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
74 (c : EMObj )
239fa20251ec field version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
75 (g : EMHom b c)
239fa20251ec field version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
76 (f : EMHom a b)
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 130
diff changeset
77 → A [ A [ φ c o FMap T (A [ (EMap g) o (EMap f) ] ) ]
113
239fa20251ec field version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
78 ≈ A [ (A [ (EMap g) o (EMap f) ]) o φ a ] ]
239fa20251ec field version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
79 Lemma-EM2 a b c g f = let
103
8dcf926482af on oging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 102
diff changeset
80 open ≈-Reasoning (A) in
101
0f7086b6a1a6 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 100
diff changeset
81 begin
113
239fa20251ec field version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
82 φ c o FMap T ((EMap g) o (EMap f))
106
4dec85377dbc yellow...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 105
diff changeset
83 ≈⟨ cdr (distr T) ⟩
113
239fa20251ec field version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
84 φ c o ( FMap T (EMap g) o FMap T (EMap f) )
106
4dec85377dbc yellow...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 105
diff changeset
85 ≈⟨ assoc ⟩
113
239fa20251ec field version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
86 ( φ c o FMap T (EMap g)) o FMap T (EMap f)
114
2032c438b6a6 EM Category constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
87 ≈⟨ car (homomorphism (g)) ⟩
113
239fa20251ec field version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
88 ( EMap g o φ b) o FMap T (EMap f)
106
4dec85377dbc yellow...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 105
diff changeset
89 ≈⟨ sym assoc ⟩
113
239fa20251ec field version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
90 EMap g o (φ b o FMap T (EMap f) )
114
2032c438b6a6 EM Category constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
91 ≈⟨ cdr (homomorphism (f)) ⟩
113
239fa20251ec field version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
92 EMap g o (EMap f o φ a)
107
da14b7f03ff8 no yellow. ready to define category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 106
diff changeset
93 ≈⟨ assoc ⟩
113
239fa20251ec field version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
94 ( (EMap g) o (EMap f) ) o φ a
101
0f7086b6a1a6 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 100
diff changeset
95 ∎
100
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
96
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 130
diff changeset
97 _∙_ : {a b c : EMObj } → EMHom b c → EMHom a b → EMHom a c
115
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
98 _∙_ {a} {b} {c} g f = record { EMap = A [ EMap g o EMap f ] ; homomorphism = Lemma-EM2 a b c g f }
111
c670d0e6b1e2 Category._o_ /= Category.Category.Id
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 110
diff changeset
99
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 130
diff changeset
100 _≗_ : {a : EMObj } {b : EMObj } (f g : EMHom a b ) → Set ℓ
113
239fa20251ec field version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
101 _≗_ f g = A [ EMap f ≈ EMap g ]
108
e763efd30868 on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 107
diff changeset
102
115
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
103 --
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
104 -- cannot use as identityL = EMidL
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
105 --
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 130
diff changeset
106 EMidL : {C D : EMObj} → {f : EMHom C D} → (EM-id ∙ f) ≗ f
115
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
107 EMidL {C} {D} {f} = let open ≈-Reasoning (A) in idL {obj D}
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 130
diff changeset
108 EMidR : {C D : EMObj} → {f : EMHom C D} → (f ∙ EM-id) ≗ f
115
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
109 EMidR {C} {_} {_} = let open ≈-Reasoning (A) in idR {obj C}
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 130
diff changeset
110 EMo-resp : {a b c : EMObj} → {f g : EMHom a b } → {h i : EMHom b c } →
115
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
111 f ≗ g → h ≗ i → (h ∙ f) ≗ (i ∙ g)
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
112 EMo-resp {a} {b} {c} {f} {g} {h} {i} = ( IsCategory.o-resp-≈ (Category.isCategory A) )
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 130
diff changeset
113 EMassoc : {a b c d : EMObj} → {f : EMHom c d } → {g : EMHom b c } → {h : EMHom a b } →
115
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
114 (f ∙ (g ∙ h)) ≗ ((f ∙ g) ∙ h)
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
115 EMassoc {_} {_} {_} {_} {f} {g} {h} = ( IsCategory.associative (Category.isCategory A) )
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
116
111
c670d0e6b1e2 Category._o_ /= Category.Category.Id
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 110
diff changeset
117 isEilenberg-MooreCategory : IsCategory EMObj EMHom _≗_ _∙_ EM-id
100
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
118 isEilenberg-MooreCategory = record { isEquivalence = isEquivalence
114
2032c438b6a6 EM Category constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
119 ; identityL = IsCategory.identityL (Category.isCategory A)
2032c438b6a6 EM Category constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
120 ; identityR = IsCategory.identityR (Category.isCategory A)
2032c438b6a6 EM Category constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
121 ; o-resp-≈ = IsCategory.o-resp-≈ (Category.isCategory A)
2032c438b6a6 EM Category constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
122 ; associative = IsCategory.associative (Category.isCategory A)
100
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
123 }
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
124 where
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
125 open ≈-Reasoning (A)
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 130
diff changeset
126 isEquivalence : {a : EMObj } {b : EMObj } →
113
239fa20251ec field version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
127 IsEquivalence {_} {_} {EMHom a b } _≗_
100
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
128 isEquivalence {C} {D} = -- this is the same function as A's equivalence but has different types
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
129 record { refl = refl-hom
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
130 ; sym = sym
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
131 ; trans = trans-hom
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
132 }
111
c670d0e6b1e2 Category._o_ /= Category.Category.Id
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 110
diff changeset
133 Eilenberg-MooreCategory : Category (c₁ ⊔ c₂ ⊔ ℓ) (c₁ ⊔ c₂ ⊔ ℓ) ℓ
c670d0e6b1e2 Category._o_ /= Category.Category.Id
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 110
diff changeset
134 Eilenberg-MooreCategory =
c670d0e6b1e2 Category._o_ /= Category.Category.Id
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 110
diff changeset
135 record { Obj = EMObj
c670d0e6b1e2 Category._o_ /= Category.Category.Id
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 110
diff changeset
136 ; Hom = EMHom
112
5f8d6d1aece4 constructed but some yellow remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
137 ; _o_ = _∙_
111
c670d0e6b1e2 Category._o_ /= Category.Category.Id
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 110
diff changeset
138 ; _≈_ = _≗_
112
5f8d6d1aece4 constructed but some yellow remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
139 ; Id = EM-id
111
c670d0e6b1e2 Category._o_ /= Category.Category.Id
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 110
diff changeset
140 ; isCategory = isEilenberg-MooreCategory
c670d0e6b1e2 Category._o_ /= Category.Category.Id
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 110
diff changeset
141 }
100
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
142
115
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
143
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
144 -- Resolution
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
145 -- T = U^T U^F
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
146 -- ε^t
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
147 -- η^T
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
148
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
149 U^T : Functor Eilenberg-MooreCategory A
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
150 U^T = record {
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 130
diff changeset
151 FObj = λ a → obj a
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 130
diff changeset
152 ; FMap = λ f → EMap f
115
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
153 ; isFunctor = record
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 130
diff changeset
154 { ≈-cong = λ eq → eq
115
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
155 ; identity = refl-hom
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
156 ; distr = refl-hom
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
157 }
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
158 } where open ≈-Reasoning (A)
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
159
116
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
160 open Monad
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 130
diff changeset
161 Lemma-EM4 : (x : Obj A ) → A [ A [ TMap μ x o TMap η (FObj T x) ] ≈ id1 A (FObj T x) ]
116
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
162 Lemma-EM4 x = let open ≈-Reasoning (A) in
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
163 begin
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
164 TMap μ x o TMap η (FObj T x)
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
165 ≈⟨ IsMonad.unity1 (isMonad M) ⟩
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
166 id1 A (FObj T x)
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
167 ∎
115
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
168
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 130
diff changeset
169 Lemma-EM5 : (x : Obj A ) → A [ A [ ( TMap μ x) o TMap μ (FObj T x) ] ≈ A [ ( TMap μ x) o FMap T ( TMap μ x) ] ]
116
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
170 Lemma-EM5 x = let open ≈-Reasoning (A) in
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
171 begin
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
172 ( TMap μ x) o TMap μ (FObj T x)
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
173 ≈⟨ IsMonad.assoc (isMonad M) ⟩
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
174 ( TMap μ x) o FMap T ( TMap μ x)
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
175 ∎
115
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
176
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 130
diff changeset
177 ftobj : Obj A → EMObj
465
d3cd28a71b3f clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
178 ftobj = λ x → record { obj = FObj T x ; φ = TMap μ x;
115
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
179 isAlgebra = record {
116
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
180 identity = Lemma-EM4 x;
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
181 eval = Lemma-EM5 x
115
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
182 } }
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
183
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 130
diff changeset
184 Lemma-EM6 : (a b : Obj A ) → (f : Hom A a b ) →
116
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
185 A [ A [ (φ (ftobj b)) o FMap T (FMap T f) ] ≈ A [ FMap T f o (φ (ftobj a)) ] ]
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
186 Lemma-EM6 a b f = let open ≈-Reasoning (A) in
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
187 begin
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
188 (φ (ftobj b)) o FMap T (FMap T f)
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
189 ≈⟨⟩
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
190 TMap μ b o FMap T (FMap T f)
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
191 ≈⟨ sym (nat μ) ⟩
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
192 FMap T f o TMap μ a
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
193 ≈⟨⟩
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
194 FMap T f o (φ (ftobj a))
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
195 ∎
115
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
196
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 130
diff changeset
197 ftmap : {a b : Obj A} → (Hom A a b) → EMHom (ftobj a) (ftobj b)
116
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
198 ftmap {a} {b} f = record { EMap = FMap T f; homomorphism = Lemma-EM6 a b f }
115
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
199
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
200 F^T : Functor A Eilenberg-MooreCategory
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
201 F^T = record {
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
202 FObj = ftobj
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
203 ; FMap = ftmap
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
204 ; isFunctor = record {
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
205 ≈-cong = ≈-cong
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
206 ; identity = identity
116
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
207 ; distr = distr1
115
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
208 }
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
209 } where
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
210 ≈-cong : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → (ftmap f) ≗ (ftmap g)
116
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
211 ≈-cong = let open ≈-Reasoning (A) in ( fcong T )
115
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
212 identity : {a : Obj A} → ftmap (id1 A a) ≗ EM-id {ftobj a}
116
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
213 identity = IsFunctor.identity ( isFunctor T )
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
214 distr1 : {a b c : Obj A} {f : Hom A a b} {g : Hom A b c} → ftmap (A [ g o f ]) ≗ ( ftmap g ∙ ftmap f )
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
215 distr1 = let open ≈-Reasoning (A) in ( distr T )
115
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
216
117
d91e89766a76 T ≃ (U^T ○ F^T)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
217 -- T = (U^T ○ F^T)
d91e89766a76 T ≃ (U^T ○ F^T)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
218
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 130
diff changeset
219 Lemma-EM7 : ∀{a b : Obj A} → (f : Hom A a b ) → A [ FMap T f ≈ FMap (U^T ○ F^T) f ]
117
d91e89766a76 T ≃ (U^T ○ F^T)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
220 Lemma-EM7 {a} {b} f = let open ≈-Reasoning (A) in
d91e89766a76 T ≃ (U^T ○ F^T)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
221 sym ( begin
d91e89766a76 T ≃ (U^T ○ F^T)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
222 FMap (U^T ○ F^T) f
d91e89766a76 T ≃ (U^T ○ F^T)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
223 ≈⟨⟩
d91e89766a76 T ≃ (U^T ○ F^T)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
224 EMap ( ftmap f )
d91e89766a76 T ≃ (U^T ○ F^T)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
225 ≈⟨⟩
d91e89766a76 T ≃ (U^T ○ F^T)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
226 FMap T f
d91e89766a76 T ≃ (U^T ○ F^T)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
227 ∎ )
d91e89766a76 T ≃ (U^T ○ F^T)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
228
d91e89766a76 T ≃ (U^T ○ F^T)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
229 Lemma-EM8 : T ≃ (U^T ○ F^T)
d91e89766a76 T ≃ (U^T ○ F^T)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
230 Lemma-EM8 f = Category.Cat.refl (Lemma-EM7 f)
d91e89766a76 T ≃ (U^T ○ F^T)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
231
d91e89766a76 T ≃ (U^T ○ F^T)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
232 η^T : NTrans A A identityFunctor ( U^T ○ F^T )
467
ba042c2d3ff5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 465
diff changeset
233 η^T = record { TMap = λ x → TMap η x ; isNTrans = record { commute = λ {a} {b} {f} → commute {a} {b} {f} }} where
ba042c2d3ff5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 465
diff changeset
234 commute : {a b : Obj A} {f : Hom A a b}
117
d91e89766a76 T ≃ (U^T ○ F^T)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
235 → A [ A [ ( FMap ( U^T ○ F^T ) f ) o ( TMap η a ) ] ≈ A [ (TMap η b ) o f ] ]
467
ba042c2d3ff5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 465
diff changeset
236 commute {a} {b} {f} = let open ≈-Reasoning (A) in
117
d91e89766a76 T ≃ (U^T ○ F^T)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
237 begin
d91e89766a76 T ≃ (U^T ○ F^T)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
238 ( FMap ( U^T ○ F^T ) f ) o ( TMap η a )
d91e89766a76 T ≃ (U^T ○ F^T)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
239 ≈⟨ sym (resp refl-hom (Lemma-EM7 f)) ⟩
d91e89766a76 T ≃ (U^T ○ F^T)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
240 FMap T f o TMap η a
d91e89766a76 T ≃ (U^T ○ F^T)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
241 ≈⟨ nat η ⟩
d91e89766a76 T ≃ (U^T ○ F^T)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
242 TMap η b o f
d91e89766a76 T ≃ (U^T ○ F^T)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
243 ∎
d91e89766a76 T ≃ (U^T ○ F^T)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
244
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 130
diff changeset
245 Lemma-EM9 : (a : EMObj) → A [ A [ (φ a) o FMap T (φ a) ] ≈ A [ (φ a) o (φ (FObj ( F^T ○ U^T ) a)) ] ]
118
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
246 Lemma-EM9 a = let open ≈-Reasoning (A) in
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
247 sym ( begin
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
248 (φ a) o (φ (FObj ( F^T ○ U^T ) a))
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
249 ≈⟨⟩
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
250 (φ a) o (TMap μ (obj a))
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
251 ≈⟨ IsAlgebra.eval (isAlgebra a) ⟩
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
252 (φ a) o FMap T (φ a)
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
253 ∎ )
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
254
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 130
diff changeset
255 emap-ε : (a : EMObj ) → EMHom (FObj ( F^T ○ U^T ) a) a
118
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
256 emap-ε a = record { EMap = φ a ; homomorphism = Lemma-EM9 a }
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
257
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
258 ε^T : NTrans Eilenberg-MooreCategory Eilenberg-MooreCategory ( F^T ○ U^T ) identityFunctor
467
ba042c2d3ff5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 465
diff changeset
259 ε^T = record { TMap = λ a → emap-ε a; isNTrans = record { commute = λ {a} {b} {f} → commute {a} {b} {f} }} where
ba042c2d3ff5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 465
diff changeset
260 commute : {a b : EMObj } {f : EMHom a b}
118
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
261 → (f ∙ ( emap-ε a ) ) ≗ (( emap-ε b ) ∙( FMap (F^T ○ U^T) f ) )
467
ba042c2d3ff5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 465
diff changeset
262 commute {a} {b} {f} = let open ≈-Reasoning (A) in
118
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
263 sym ( begin
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
264 EMap (( emap-ε b ) ∙ ( FMap (F^T ○ U^T) f ))
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
265 ≈⟨⟩
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
266 φ b o FMap T (EMap f)
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
267 ≈⟨ homomorphism f ⟩
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
268 EMap f o φ a
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
269 ≈⟨⟩
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
270 EMap (f ∙ ( emap-ε a ))
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
271 ∎ )
467
ba042c2d3ff5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 465
diff changeset
272
118
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
273 --
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
274 -- μ = U^T ε U^F
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
275 --
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
276
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 130
diff changeset
277 emap-μ : (a : Obj A) → Hom A (FObj ( U^T ○ F^T ) (FObj ( U^T ○ F^T ) a)) (FObj ( U^T ○ F^T ) a)
118
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
278 emap-μ a = FMap U^T ( TMap ε^T ( FObj F^T a ))
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
279
120
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
280 μ^T : NTrans A A (( U^T ○ F^T ) ○ ( U^T ○ F^T )) ( U^T ○ F^T )
467
ba042c2d3ff5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 465
diff changeset
281 μ^T = record { TMap = emap-μ ; isNTrans = record { commute = commute }} where
ba042c2d3ff5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 465
diff changeset
282 commute : {a b : Obj A} {f : Hom A a b}
118
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
283 → A [ A [ (FMap (U^T ○ F^T) f) o ( emap-μ a) ] ≈ A [ ( emap-μ b ) o FMap (U^T ○ F^T) ( FMap (U^T ○ F^T) f) ] ]
467
ba042c2d3ff5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 465
diff changeset
284 commute {a} {b} {f} = let open ≈-Reasoning (A) in
119
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
285 sym ( begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
286 ( emap-μ b ) o FMap (U^T ○ F^T) ( FMap (U^T ○ F^T) f)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
287 ≈⟨⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
288 (FMap U^T ( TMap ε^T ( FObj F^T b ))) o (FMap (U^T ○ F^T) ( FMap (U^T ○ F^T) f) )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
289 ≈⟨⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
290 (TMap μ b) o (FMap T (FMap T f))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
291 ≈⟨ sym (nat μ) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
292 FMap T f o ( TMap μ a )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
293 ≈⟨⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
294 (FMap (U^T ○ F^T) f) o ( emap-μ a)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
295 ∎ )
118
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
296
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 130
diff changeset
297 Lemma-EM10 : {x : Obj A } → A [ TMap μ^T x ≈ FMap U^T ( TMap ε^T ( FObj F^T x ) ) ]
120
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
298 Lemma-EM10 {x} = let open ≈-Reasoning (A) in
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
299 sym ( begin
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
300 FMap U^T ( TMap ε^T ( FObj F^T x ) )
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
301 ≈⟨⟩
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
302 emap-μ x
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
303 ≈⟨⟩
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
304 TMap μ^T x
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
305 ∎ )
117
d91e89766a76 T ≃ (U^T ○ F^T)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
306
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 130
diff changeset
307 Lemma-EM11 : {x : Obj A } → A [ TMap μ x ≈ FMap U^T ( TMap ε^T ( FObj F^T x ) ) ]
120
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
308 Lemma-EM11 {x} = let open ≈-Reasoning (A) in
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
309 sym ( begin
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
310 FMap U^T ( TMap ε^T ( FObj F^T x ) )
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
311 ≈⟨⟩
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
312 TMap μ x
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
313 ∎ )
116
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
314
120
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
315 Adj^T : Adjunction A Eilenberg-MooreCategory U^T F^T η^T ε^T
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
316 Adj^T = record {
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
317 isAdjunction = record {
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 130
diff changeset
318 adjoint1 = λ {b} → IsAlgebra.identity (isAlgebra b) ; -- adjoint1
120
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
319 adjoint2 = adjoint2
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
320 }
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
321 } where
122
f8fbd5ecec97 no yellow on em-category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 120
diff changeset
322 adjoint1 : { b : EMObj } →
120
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
323 A [ A [ ( FMap U^T ( TMap ε^T b)) o ( TMap η^T ( FObj U^T b )) ] ≈ id1 A (FObj U^T b) ]
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
324 adjoint1 {b} = let open ≈-Reasoning (A) in
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
325 begin
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
326 ( FMap U^T ( TMap ε^T b)) o ( TMap η^T ( FObj U^T b ))
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
327 ≈⟨⟩
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
328 φ b o TMap η (obj b)
122
f8fbd5ecec97 no yellow on em-category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 120
diff changeset
329 ≈⟨ IsAlgebra.identity (isAlgebra b) ⟩
465
d3cd28a71b3f clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
330 id1 A (obj b)
122
f8fbd5ecec97 no yellow on em-category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 120
diff changeset
331 ≈⟨⟩
f8fbd5ecec97 no yellow on em-category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 120
diff changeset
332 id1 A (FObj U^T b)
120
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
333 ∎
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
334 adjoint2 : {a : Obj A} →
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
335 Eilenberg-MooreCategory [ Eilenberg-MooreCategory [ ( TMap ε^T ( FObj F^T a )) o ( FMap F^T ( TMap η^T a )) ]
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
336 ≈ id1 Eilenberg-MooreCategory (FObj F^T a) ]
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
337 adjoint2 {a} = let open ≈-Reasoning (A) in
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
338 begin
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
339 EMap (( TMap ε^T ( FObj F^T a )) ∙ ( FMap F^T ( TMap η^T a )) )
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
340 ≈⟨⟩
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
341 TMap μ a o FMap T ( TMap η a )
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
342 ≈⟨ IsMonad.unity2 (isMonad M) ⟩
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
343 EMap (id1 Eilenberg-MooreCategory (FObj F^T a))
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
344 ∎
115
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
345
120
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
346 open MResolution
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
347
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
348 Resolution^T : MResolution A Eilenberg-MooreCategory T U^T F^T {η^T} {ε^T} {μ^T} Adj^T
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
349 Resolution^T = record {
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
350 T=UF = Lemma-EM8;
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
351 μ=UεF = Lemma-EM11
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
352 }
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
353
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
354
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
355 -- end