Mercurial > hg > Members > kono > Proof > category

annotate em-category.agda @ 130:5f331dfc000b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
remove Kleisli record
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 08 Aug 2013 22:05:41 +0900
parents f8fbd5ecec97
children d6a6dd305da2
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
114
2032c438b6a6 EM Category constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
42 a : Obj A
2032c438b6a6 EM Category constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
43 phi : Hom A (FObj T a) a
2032c438b6a6 EM Category constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
44 isAlgebra : IsAlgebra {a} {phi}
105
b881dbc47684 on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
45 obj : Obj A
b881dbc47684 on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
46 obj = a
113
239fa20251ec field version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
47 φ : Hom A (FObj T a) a
239fa20251ec field version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
48 φ = phi
108
e763efd30868 on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 107
diff changeset
49 open EMObj
104
53a79dfdcd04 problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
50
113
239fa20251ec field version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
51 record Eilenberg-Moore-Hom (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
52 field
113
239fa20251ec field version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
53 EMap : Hom A (obj a) (obj b)
114
2032c438b6a6 EM Category constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
54 homomorphism : A [ A [ (φ b) o FMap T EMap ] ≈ A [ EMap o (φ a) ] ]
104
53a79dfdcd04 problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
55 open Eilenberg-Moore-Hom
105
b881dbc47684 on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
56
113
239fa20251ec field version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
57 EMHom : (a : EMObj ) (b : EMObj ) -> Set (c₁ ⊔ c₂ ⊔ ℓ)
239fa20251ec field version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
58 EMHom = \a b -> Eilenberg-Moore-Hom a b
100
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
59
113
239fa20251ec field version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
60 Lemma-EM1 : {x : Obj A} {φ : Hom A (FObj T x) x} (a : EMObj )
101
0f7086b6a1a6 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 100
diff changeset
61 -> 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
62 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
63 begin
0f7086b6a1a6 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 100
diff changeset
64 φ o FMap T (id1 A x)
0f7086b6a1a6 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 100
diff changeset
65 ≈⟨ cdr ( IsFunctor.identity (isFunctor T) ) ⟩
0f7086b6a1a6 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 100
diff changeset
66 φ o (id1 A (FObj T x))
0f7086b6a1a6 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 100
diff changeset
67 ≈⟨ idR ⟩
0f7086b6a1a6 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 100
diff changeset
68 φ
0f7086b6a1a6 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 100
diff changeset
69 ≈⟨ sym idL ⟩
0f7086b6a1a6 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 100
diff changeset
70 (id1 A x) o φ
0f7086b6a1a6 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 100
diff changeset
71 ∎
0f7086b6a1a6 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 100
diff changeset
72
113
239fa20251ec field version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
73 EM-id : { a : EMObj } -> EMHom a a
239fa20251ec field version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
74 EM-id {a} = record { EMap = id1 A (obj a);
114
2032c438b6a6 EM Category constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
75 homomorphism = Lemma-EM1 {obj a} {phi a} a }
100
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
76
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
77 open import Relation.Binary.Core
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
78
113
239fa20251ec field version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
79 Lemma-EM2 : (a : EMObj )
239fa20251ec field version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
80 (b : EMObj )
239fa20251ec field version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
81 (c : EMObj )
239fa20251ec field version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
82 (g : EMHom b c)
239fa20251ec field version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
83 (f : EMHom a b)
239fa20251ec field version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
84 -> A [ A [ φ c o FMap T (A [ (EMap g) o (EMap f) ] ) ]
239fa20251ec field version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
85 ≈ A [ (A [ (EMap g) o (EMap f) ]) o φ a ] ]
239fa20251ec field version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
86 Lemma-EM2 a b c g f = let
103
8dcf926482af on oging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 102
diff changeset
87 open ≈-Reasoning (A) in
101
0f7086b6a1a6 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 100
diff changeset
88 begin
113
239fa20251ec field version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
89 φ c o FMap T ((EMap g) o (EMap f))
106
4dec85377dbc yellow...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 105
diff changeset
90 ≈⟨ cdr (distr T) ⟩
113
239fa20251ec field version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
91 φ 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
92 ≈⟨ assoc ⟩
113
239fa20251ec field version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
93 ( φ 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
94 ≈⟨ car (homomorphism (g)) ⟩
113
239fa20251ec field version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
95 ( EMap g o φ b) o FMap T (EMap f)
106
4dec85377dbc yellow...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 105
diff changeset
96 ≈⟨ sym assoc ⟩
113
239fa20251ec field version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
97 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
98 ≈⟨ cdr (homomorphism (f)) ⟩
113
239fa20251ec field version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
99 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
100 ≈⟨ assoc ⟩
113
239fa20251ec field version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
101 ( (EMap g) o (EMap f) ) o φ a
101
0f7086b6a1a6 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 100
diff changeset
102 ∎
100
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
103
114
2032c438b6a6 EM Category constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
104 _∙_ : {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
105 _∙_ {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
106
114
2032c438b6a6 EM Category constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
107 _≗_ : {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
108 _≗_ f g = A [ EMap f ≈ EMap g ]
108
e763efd30868 on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 107
diff changeset
109
115
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
110 --
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
111 -- 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
112 --
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
113 EMidL : {C D : EMObj} -> {f : EMHom C D} → (EM-id ∙ f) ≗ f
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
114 EMidL {C} {D} {f} = let open ≈-Reasoning (A) in idL {obj D}
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
115 EMidR : {C D : EMObj} -> {f : EMHom C D} → (f ∙ EM-id) ≗ f
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
116 EMidR {C} {_} {_} = let open ≈-Reasoning (A) in idR {obj C}
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
117 EMo-resp : {a b c : EMObj} -> {f g : EMHom a b } → {h i : EMHom b c } →
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
118 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
119 EMo-resp {a} {b} {c} {f} {g} {h} {i} = ( IsCategory.o-resp-≈ (Category.isCategory A) )
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
120 EMassoc : {a b c d : EMObj} -> {f : EMHom c d } → {g : EMHom b c } → {h : EMHom a b } →
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
121 (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
122 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
123
111
c670d0e6b1e2 Category._o_ /= Category.Category.Id
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 110
diff changeset
124 isEilenberg-MooreCategory : IsCategory EMObj EMHom _≗_ _∙_ EM-id
100
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
125 isEilenberg-MooreCategory = record { isEquivalence = isEquivalence
114
2032c438b6a6 EM Category constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
126 ; identityL = IsCategory.identityL (Category.isCategory A)
2032c438b6a6 EM Category constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
127 ; identityR = IsCategory.identityR (Category.isCategory A)
2032c438b6a6 EM Category constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
128 ; o-resp-≈ = IsCategory.o-resp-≈ (Category.isCategory A)
2032c438b6a6 EM Category constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
129 ; associative = IsCategory.associative (Category.isCategory A)
100
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
130 }
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
131 where
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
132 open ≈-Reasoning (A)
113
239fa20251ec field version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
133 isEquivalence : {a : EMObj } {b : EMObj } ->
239fa20251ec field version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
134 IsEquivalence {_} {_} {EMHom a b } _≗_
100
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
135 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
136 record { refl = refl-hom
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
137 ; sym = sym
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
138 ; trans = trans-hom
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
139 }
111
c670d0e6b1e2 Category._o_ /= Category.Category.Id
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 110
diff changeset
140 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
141 Eilenberg-MooreCategory =
c670d0e6b1e2 Category._o_ /= Category.Category.Id
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 110
diff changeset
142 record { Obj = EMObj
c670d0e6b1e2 Category._o_ /= Category.Category.Id
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 110
diff changeset
143 ; Hom = EMHom
112
5f8d6d1aece4 constructed but some yellow remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
144 ; _o_ = _∙_
111
c670d0e6b1e2 Category._o_ /= Category.Category.Id
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 110
diff changeset
145 ; _≈_ = _≗_
112
5f8d6d1aece4 constructed but some yellow remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
146 ; Id = EM-id
111
c670d0e6b1e2 Category._o_ /= Category.Category.Id
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 110
diff changeset
147 ; isCategory = isEilenberg-MooreCategory
c670d0e6b1e2 Category._o_ /= Category.Category.Id
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 110
diff changeset
148 }
100
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
149
115
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
150
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
151 -- Resolution
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
152 -- 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
153 -- ε^t
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
154 -- η^T
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
155
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
156 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
157 U^T = record {
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
158 FObj = \a -> obj a
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
159 ; FMap = \f -> EMap f
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
160 ; isFunctor = record
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
161 { ≈-cong = \eq -> eq
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
162 ; identity = refl-hom
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
163 ; distr = refl-hom
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
164 }
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
165 } where open ≈-Reasoning (A)
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
166
116
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
167 open Monad
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
168 Lemma-EM4 : (x : Obj A ) -> A [ A [ TMap μ x o TMap η (FObj T x) ] ≈ id1 A (FObj T x) ]
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
169 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
170 begin
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
171 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
172 ≈⟨ IsMonad.unity1 (isMonad M) ⟩
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
173 id1 A (FObj T x)
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
174 ∎
115
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
175
116
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
176 Lemma-EM5 : (x : Obj A ) -> A [ A [ ( TMap μ x) o TMap μ (FObj T x) ] ≈ A [ ( 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
177 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
178 begin
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
179 ( 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
180 ≈⟨ IsMonad.assoc (isMonad M) ⟩
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
181 ( 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
182 ∎
115
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
183
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
184 ftobj : Obj A -> EMObj
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
185 ftobj = \x -> record { a = FObj T x ; phi = TMap μ x;
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
186 isAlgebra = record {
116
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
187 identity = Lemma-EM4 x;
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
188 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
189 } }
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
190
116
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
191 Lemma-EM6 : (a b : Obj A ) -> (f : Hom A a b ) ->
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
192 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
193 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
194 begin
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
195 (φ (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
196 ≈⟨⟩
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
197 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
198 ≈⟨ sym (nat μ) ⟩
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
199 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
200 ≈⟨⟩
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
201 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
202 ∎
115
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
203
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
204 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
205 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
206
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
207 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
208 F^T = record {
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
209 FObj = ftobj
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
210 ; FMap = ftmap
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
211 ; isFunctor = record {
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
212 ≈-cong = ≈-cong
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
213 ; identity = identity
116
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
214 ; distr = distr1
115
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
215 }
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
216 } where
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
217 ≈-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
218 ≈-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
219 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
220 identity = IsFunctor.identity ( isFunctor T )
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
221 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
222 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
223
117
d91e89766a76 T ≃ (U^T ○ F^T)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
224 -- T = (U^T ○ F^T)
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 Lemma-EM7 : ∀{a b : Obj A} -> (f : Hom A a b ) -> A [ FMap T f ≈ FMap (U^T ○ F^T) f ]
d91e89766a76 T ≃ (U^T ○ F^T)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
227 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
228 sym ( begin
d91e89766a76 T ≃ (U^T ○ F^T)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
229 FMap (U^T ○ F^T) f
d91e89766a76 T ≃ (U^T ○ F^T)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
230 ≈⟨⟩
d91e89766a76 T ≃ (U^T ○ F^T)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
231 EMap ( ftmap f )
d91e89766a76 T ≃ (U^T ○ F^T)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
232 ≈⟨⟩
d91e89766a76 T ≃ (U^T ○ F^T)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
233 FMap T f
d91e89766a76 T ≃ (U^T ○ F^T)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
234 ∎ )
d91e89766a76 T ≃ (U^T ○ F^T)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
235
d91e89766a76 T ≃ (U^T ○ F^T)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
236 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
237 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
238
d91e89766a76 T ≃ (U^T ○ F^T)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
239 η^T : NTrans A A identityFunctor ( U^T ○ F^T )
d91e89766a76 T ≃ (U^T ○ F^T)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
240 η^T = record { TMap = \x -> TMap η x ; isNTrans = isNTrans1 } where
130
5f331dfc000b remove Kleisli record
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 122
diff changeset
241 commute1 : {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
242 → A [ A [ ( FMap ( U^T ○ F^T ) f ) o ( TMap η a ) ] ≈ A [ (TMap η b ) o f ] ]
130
5f331dfc000b remove Kleisli record
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 122
diff changeset
243 commute1 {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
244 begin
d91e89766a76 T ≃ (U^T ○ F^T)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
245 ( 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
246 ≈⟨ 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
247 FMap T f o TMap η a
d91e89766a76 T ≃ (U^T ○ F^T)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
248 ≈⟨ nat η ⟩
d91e89766a76 T ≃ (U^T ○ F^T)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
249 TMap η b o f
d91e89766a76 T ≃ (U^T ○ F^T)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
250 ∎
d91e89766a76 T ≃ (U^T ○ F^T)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
251 isNTrans1 : IsNTrans A A identityFunctor ( U^T ○ F^T ) (\a -> TMap η a)
130
5f331dfc000b remove Kleisli record
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 122
diff changeset
252 isNTrans1 = record { commute = commute1 }
117
d91e89766a76 T ≃ (U^T ○ F^T)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
253
118
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
254 Lemma-EM9 : (a : EMObj) -> A [ A [ (φ a) o FMap T (φ a) ] ≈ A [ (φ a) o (φ (FObj ( F^T ○ U^T ) a)) ] ]
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
255 Lemma-EM9 a = let open ≈-Reasoning (A) in
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
256 sym ( begin
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
257 (φ a) o (φ (FObj ( F^T ○ U^T ) a))
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
258 ≈⟨⟩
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
259 (φ a) o (TMap μ (obj a))
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
260 ≈⟨ IsAlgebra.eval (isAlgebra a) ⟩
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
261 (φ a) o FMap T (φ a)
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
262 ∎ )
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
263
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
264 emap-ε : (a : EMObj ) -> EMHom (FObj ( F^T ○ U^T ) a) a
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
265 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
266
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
267 ε^T : NTrans Eilenberg-MooreCategory Eilenberg-MooreCategory ( F^T ○ U^T ) identityFunctor
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
268 ε^T = record { TMap = \a -> emap-ε a; isNTrans = isNTrans1 } where
130
5f331dfc000b remove Kleisli record
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 122
diff changeset
269 commute1 : {a b : EMObj } {f : EMHom a b}
118
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
270 → (f ∙ ( emap-ε a ) ) ≗ (( emap-ε b ) ∙( FMap (F^T ○ U^T) f ) )
130
5f331dfc000b remove Kleisli record
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 122
diff changeset
271 commute1 {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
272 sym ( begin
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
273 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
274 ≈⟨⟩
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
275 φ b o FMap T (EMap f)
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
276 ≈⟨ homomorphism f ⟩
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
277 EMap f o φ a
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
278 ≈⟨⟩
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
279 EMap (f ∙ ( emap-ε a ))
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
280 ∎ )
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
281 isNTrans1 : IsNTrans Eilenberg-MooreCategory Eilenberg-MooreCategory ( F^T ○ U^T ) identityFunctor (\a -> emap-ε a )
130
5f331dfc000b remove Kleisli record
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 122
diff changeset
282 isNTrans1 = record { commute = \{a} {b} {f} -> (IsEquivalence.sym (IsCategory.isEquivalence (Category.isCategory A)) ) (homomorphism f ) } -- naturity1 {a} {b} {f}
118
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
283
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
284 --
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
285 -- μ = U^T ε U^F
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
286 --
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
287
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
288 emap-μ : (a : Obj A) -> Hom A (FObj ( U^T ○ F^T ) (FObj ( U^T ○ F^T ) a)) (FObj ( U^T ○ F^T ) a)
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
289 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
290
120
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
291 μ^T : NTrans A A (( U^T ○ F^T ) ○ ( U^T ○ F^T )) ( U^T ○ F^T )
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
292 μ^T = record { TMap = emap-μ ; isNTrans = isNTrans1 } where
130
5f331dfc000b remove Kleisli record
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 122
diff changeset
293 commute1 : {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
294 → 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) ] ]
130
5f331dfc000b remove Kleisli record
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 122
diff changeset
295 commute1 {a} {b} {f} = let open ≈-Reasoning (A) in
119
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
296 sym ( begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
297 ( 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
298 ≈⟨⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
299 (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
300 ≈⟨⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
301 (TMap μ b) o (FMap T (FMap T f))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
302 ≈⟨ sym (nat μ) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
303 FMap T f o ( TMap μ a )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
304 ≈⟨⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
305 (FMap (U^T ○ F^T) f) o ( emap-μ a)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
306 ∎ )
118
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
307 isNTrans1 : IsNTrans A A (( U^T ○ F^T ) ○ ( U^T ○ F^T )) ( U^T ○ F^T ) emap-μ
130
5f331dfc000b remove Kleisli record
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 122
diff changeset
308 isNTrans1 = record { commute = commute1 }
118
324950507362 ε^T and μ^t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
309
120
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
310 Lemma-EM10 : {x : Obj A } -> A [ TMap μ^T x ≈ 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 Lemma-EM10 {x} = let open ≈-Reasoning (A) in
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
312 sym ( begin
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
313 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
314 ≈⟨⟩
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
315 emap-μ x
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
316 ≈⟨⟩
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
317 TMap μ^T x
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
318 ∎ )
117
d91e89766a76 T ≃ (U^T ○ F^T)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
319
120
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
320 Lemma-EM11 : {x : Obj A } -> A [ TMap μ x ≈ 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
321 Lemma-EM11 {x} = let open ≈-Reasoning (A) in
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
322 sym ( begin
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
323 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
324 ≈⟨⟩
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
325 TMap μ x
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
326 ∎ )
116
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
327
120
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
328 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
329 Adj^T = record {
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
330 isAdjunction = record {
122
f8fbd5ecec97 no yellow on em-category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 120
diff changeset
331 adjoint1 = \{b} -> IsAlgebra.identity (isAlgebra b) ; -- adjoint1
120
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
332 adjoint2 = adjoint2
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 } where
122
f8fbd5ecec97 no yellow on em-category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 120
diff changeset
335 adjoint1 : { b : EMObj } →
120
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
336 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
337 adjoint1 {b} = 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 ( 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
340 ≈⟨⟩
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
341 φ b o TMap η (obj b)
122
f8fbd5ecec97 no yellow on em-category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 120
diff changeset
342 ≈⟨ IsAlgebra.identity (isAlgebra b) ⟩
f8fbd5ecec97 no yellow on em-category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 120
diff changeset
343 id1 A (a b)
f8fbd5ecec97 no yellow on em-category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 120
diff changeset
344 ≈⟨⟩
f8fbd5ecec97 no yellow on em-category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 120
diff changeset
345 id1 A (FObj U^T b)
120
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
346 ∎
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
347 adjoint2 : {a : Obj A} →
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
348 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
349 ≈ id1 Eilenberg-MooreCategory (FObj F^T a) ]
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
350 adjoint2 {a} = let open ≈-Reasoning (A) in
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
351 begin
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
352 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
353 ≈⟨⟩
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
354 TMap μ a o FMap T ( TMap η a )
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
355 ≈⟨ IsMonad.unity2 (isMonad M) ⟩
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
356 EMap (id1 Eilenberg-MooreCategory (FObj F^T a))
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
357 ∎
115
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
358
120
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
359 open MResolution
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
360
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
361 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
362 Resolution^T = record {
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
363 T=UF = Lemma-EM8;
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
364 μ=UεF = Lemma-EM11
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
365 }
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
366
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
367
494f870ad54b EM Resolution complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
368 -- end