Mercurial > hg > Members > kono > Proof > category

annotate em-category.agda @ 116:0e37b2cf3c73

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
F^T and U^T constructed
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 01 Aug 2013 09:24:53 +0900
parents 17e69b05bc5e
children d91e89766a76
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
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
224 --open MResolution
116
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
225
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
226 --Resolution^T : MResolution A Eilenberg-MooreCategory T^U_T F^T {η^t} {ε^T} {μ^T} Adj_T
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
227 --Resolution^T = record {
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
228 -- T=UF = Lemma-EM7;
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
229 -- μ=UεF = Lemma-EM8
0e37b2cf3c73 F^T and U^T constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
230 --}
115
17e69b05bc5e U^T and F^T problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
231
100
59dec035602c Eilenberg-Moore Category start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
232 -- -- end