annotate kleisli.agda @ 790:1e7319868d77

Sets is CCC
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 19 Apr 2019 23:42:19 +0900
parents a5f2ca67e7c5
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
82
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
1 -- -- -- -- -- -- -- --
153
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 152
diff changeset
2 -- Monad to Kelisli Category
82
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
3 -- defines U_T and F_T as a resolution of Monad
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
4 -- checks Adjointness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
5 --
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
6 -- Shinji KONO <kono@ie.u-ryukyu.ac.jp>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
7 -- -- -- -- -- -- -- --
0
302941542c0f category agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8
302941542c0f category agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 -- Monad
302941542c0f category agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 -- Category A
302941542c0f category agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 -- A = Category
22
b3cb592d7b9d add some law
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
12 -- Functor T : A → A
0
302941542c0f category agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 --T(a) = t(a)
302941542c0f category agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 --T(f) = tf(f)
302941542c0f category agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15
2
7ce421d5ee2b unity1 unity2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
16 open import Category -- https://github.com/konn/category-agda
0
302941542c0f category agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 open import Level
56
83ff8d48fdca add unitility
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 31
diff changeset
18 --open import Category.HomReasoning
83ff8d48fdca add unitility
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 31
diff changeset
19 open import HomReasoning
83ff8d48fdca add unitility
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 31
diff changeset
20 open import cat-utility
72
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 71
diff changeset
21 open import Category.Cat
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 71
diff changeset
22
152
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 130
diff changeset
23 module kleisli { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ }
72
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 71
diff changeset
24 { T : Functor A A }
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 71
diff changeset
25 { η : NTrans A A identityFunctor T }
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 71
diff changeset
26 { μ : NTrans A A (T ○ T) T }
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 474
diff changeset
27 { M : IsMonad A T η μ } where
0
302941542c0f category agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28
1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
29 --T(g f) = T(g) T(f)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
30
31
17b8bafebad7 add universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 30
diff changeset
31 open Functor
22
b3cb592d7b9d add some law
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
32 Lemma1 : {c₁ c₂ l : Level} {A : Category c₁ c₂ l} (T : Functor A A) → {a b c : Obj A} {g : Hom A b c} { f : Hom A a b }
b3cb592d7b9d add some law
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
33 → A [ ( FMap T (A [ g o f ] )) ≈ (A [ FMap T g o FMap T f ]) ]
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
34 Lemma1 = λ t → IsFunctor.distr ( isFunctor t )
0
302941542c0f category agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35
302941542c0f category agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36
7
79d9c30e995a Reasoning
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
37 open NTrans
1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
38 Lemma2 : {c₁ c₂ l : Level} {A : Category c₁ c₂ l} {F G : Functor A A}
22
b3cb592d7b9d add some law
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
39 → (μ : NTrans A A F G) → {a b : Obj A} { f : Hom A a b }
30
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 29
diff changeset
40 → A [ A [ FMap G f o TMap μ a ] ≈ A [ TMap μ b o FMap F f ] ]
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
41 Lemma2 = λ n → IsNTrans.commute ( isNTrans n )
0
302941542c0f category agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42
82
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
43 -- Laws of Monad
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
44 --
22
b3cb592d7b9d add some law
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
45 -- η : 1_A → T
b3cb592d7b9d add some law
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
46 -- μ : TT → T
82
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
47 -- μ(a)η(T(a)) = a -- unity law 1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
48 -- μ(a)T(η(a)) = a -- unity law 2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
49 -- μ(a)(μ(T(a))) = μ(a)T(μ(a)) -- association law
0
302941542c0f category agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
50
302941542c0f category agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
51
2
7ce421d5ee2b unity1 unity2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
52 Lemma3 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ}
7ce421d5ee2b unity1 unity2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
53 { T : Functor A A }
7
79d9c30e995a Reasoning
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
54 { η : NTrans A A identityFunctor T }
79d9c30e995a Reasoning
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
55 { μ : NTrans A A (T ○ T) T }
22
b3cb592d7b9d add some law
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
56 { a : Obj A } →
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 474
diff changeset
57 ( M : IsMonad A T η μ )
30
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 29
diff changeset
58 → A [ A [ TMap μ a o TMap μ ( FObj T a ) ] ≈ A [ TMap μ a o FMap T (TMap μ a) ] ]
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 474
diff changeset
59 Lemma3 = λ m → IsMonad.assoc m
2
7ce421d5ee2b unity1 unity2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
60
7ce421d5ee2b unity1 unity2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
61
7ce421d5ee2b unity1 unity2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
62 Lemma4 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A } { f : Hom A a b}
22
b3cb592d7b9d add some law
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
63 → A [ A [ Id {_} {_} {_} {A} b o f ] ≈ f ]
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
64 Lemma4 = λ a → IsCategory.identityL ( Category.isCategory a )
0
302941542c0f category agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
65
3
dce706edd66b Kleisli
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 2
diff changeset
66 Lemma5 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ}
dce706edd66b Kleisli
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 2
diff changeset
67 { T : Functor A A }
7
79d9c30e995a Reasoning
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
68 { η : NTrans A A identityFunctor T }
79d9c30e995a Reasoning
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
69 { μ : NTrans A A (T ○ T) T }
22
b3cb592d7b9d add some law
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
70 { a : Obj A } →
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 474
diff changeset
71 ( M : IsMonad A T η μ )
30
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 29
diff changeset
72 → A [ A [ TMap μ a o TMap η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 474
diff changeset
73 Lemma5 = λ m → IsMonad.unity1 m
3
dce706edd66b Kleisli
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 2
diff changeset
74
dce706edd66b Kleisli
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 2
diff changeset
75 Lemma6 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ}
dce706edd66b Kleisli
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 2
diff changeset
76 { T : Functor A A }
7
79d9c30e995a Reasoning
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
77 { η : NTrans A A identityFunctor T }
79d9c30e995a Reasoning
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
78 { μ : NTrans A A (T ○ T) T }
22
b3cb592d7b9d add some law
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
79 { a : Obj A } →
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 474
diff changeset
80 ( M : IsMonad A T η μ )
30
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 29
diff changeset
81 → A [ A [ TMap μ a o (FMap T (TMap η a )) ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 474
diff changeset
82 Lemma6 = λ m → IsMonad.unity2 m
3
dce706edd66b Kleisli
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 2
diff changeset
83
82
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
84 -- Laws of Kleisli Category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
85 --
0
302941542c0f category agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
86 -- nat of η
82
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
87 -- g ○ f = μ(c) T(g) f -- join definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
88 -- η(b) ○ f = f -- left id (Lemma7)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
89 -- f ○ η(a) = f -- right id (Lemma8)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
90 -- h ○ (g ○ f) = (h ○ g) ○ f -- assocation law (Lemma9)
11
2cbecadc56c1 reasoning test
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
91
22
b3cb592d7b9d add some law
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
92 -- η(b) ○ f = f
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 474
diff changeset
93
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 474
diff changeset
94 join : (m : IsMonad A T η μ ) → { a b : Obj A } → { c : Obj A } →
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 474
diff changeset
95 ( Hom A b ( FObj T c )) → ( Hom A a ( FObj T b)) → Hom A a ( FObj T c )
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 474
diff changeset
96 join _ {_} {_} {c} g f = A [ TMap μ c o A [ FMap T g o f ] ]
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 474
diff changeset
97
73
b75b5792bd81 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 72
diff changeset
98 Lemma7 : { a : Obj A } { b : Obj A } ( f : Hom A a ( FObj T b) )
130
5f331dfc000b remove Kleisli record
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 108
diff changeset
99 → A [ join M (TMap η b) f ≈ f ]
73
b75b5792bd81 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 72
diff changeset
100 Lemma7 {_} {b} f =
b75b5792bd81 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 72
diff changeset
101 let open ≈-Reasoning (A) in
21
a7b0f7ab9881 unity law 1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 19
diff changeset
102 begin
130
5f331dfc000b remove Kleisli record
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 108
diff changeset
103 join M (TMap η b) f
21
a7b0f7ab9881 unity law 1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 19
diff changeset
104 ≈⟨ refl-hom ⟩
73
b75b5792bd81 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 72
diff changeset
105 A [ TMap μ b o A [ FMap T ((TMap η b)) o f ] ]
b75b5792bd81 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 72
diff changeset
106 ≈⟨ IsCategory.associative (Category.isCategory A) ⟩
b75b5792bd81 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 72
diff changeset
107 A [ A [ TMap μ b o FMap T ((TMap η b)) ] o f ]
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 474
diff changeset
108 ≈⟨ car ( IsMonad.unity2 M ) ⟩
73
b75b5792bd81 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 72
diff changeset
109 A [ id (FObj T b) o f ]
b75b5792bd81 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 72
diff changeset
110 ≈⟨ IsCategory.identityL (Category.isCategory A) ⟩
21
a7b0f7ab9881 unity law 1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 19
diff changeset
111 f
a7b0f7ab9881 unity law 1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 19
diff changeset
112
7
79d9c30e995a Reasoning
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
113
22
b3cb592d7b9d add some law
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
114 -- f ○ η(a) = f
73
b75b5792bd81 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 72
diff changeset
115 Lemma8 : { a : Obj A } { b : Obj A }
22
b3cb592d7b9d add some law
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
116 ( f : Hom A a ( FObj T b) )
130
5f331dfc000b remove Kleisli record
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 108
diff changeset
117 → A [ join M f (TMap η a) ≈ f ]
73
b75b5792bd81 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 72
diff changeset
118 Lemma8 {a} {b} f =
22
b3cb592d7b9d add some law
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
119 begin
130
5f331dfc000b remove Kleisli record
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 108
diff changeset
120 join M f (TMap η a)
22
b3cb592d7b9d add some law
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
121 ≈⟨ refl-hom ⟩
72
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 71
diff changeset
122 A [ TMap μ b o A [ FMap T f o (TMap η a) ] ]
66
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 63
diff changeset
123 ≈⟨ cdr ( nat η ) ⟩
72
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 71
diff changeset
124 A [ TMap μ b o A [ (TMap η ( FObj T b)) o f ] ]
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 71
diff changeset
125 ≈⟨ IsCategory.associative (Category.isCategory A) ⟩
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 71
diff changeset
126 A [ A [ TMap μ b o (TMap η ( FObj T b)) ] o f ]
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 474
diff changeset
127 ≈⟨ car ( IsMonad.unity1 M ) ⟩
72
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 71
diff changeset
128 A [ id (FObj T b) o f ]
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 71
diff changeset
129 ≈⟨ IsCategory.identityL (Category.isCategory A) ⟩
22
b3cb592d7b9d add some law
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
130 f
b3cb592d7b9d add some law
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
131 ∎ where
72
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 71
diff changeset
132 open ≈-Reasoning (A)
5
16572013c362 Kleisli Proposition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
133
22
b3cb592d7b9d add some law
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
134 -- h ○ (g ○ f) = (h ○ g) ○ f
72
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 71
diff changeset
135 Lemma9 : { a b c d : Obj A }
73
b75b5792bd81 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 72
diff changeset
136 ( h : Hom A c ( FObj T d) )
23
736df1a35807 join assoc on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 22
diff changeset
137 ( g : Hom A b ( FObj T c) )
73
b75b5792bd81 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 72
diff changeset
138 ( f : Hom A a ( FObj T b) )
130
5f331dfc000b remove Kleisli record
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 108
diff changeset
139 → A [ join M h (join M g f) ≈ join M ( join M h g) f ]
73
b75b5792bd81 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 72
diff changeset
140 Lemma9 {a} {b} {c} {d} h g f =
24
171c31acf78e on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
141 begin
130
5f331dfc000b remove Kleisli record
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 108
diff changeset
142 join M h (join M g f)
30
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 29
diff changeset
143 ≈⟨⟩
130
5f331dfc000b remove Kleisli record
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 108
diff changeset
144 join M h ( ( TMap μ c o ( FMap T g o f ) ) )
28
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 27
diff changeset
145 ≈⟨ refl-hom ⟩
30
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 29
diff changeset
146 ( TMap μ d o ( FMap T h o ( TMap μ c o ( FMap T g o f ) ) ) )
28
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 27
diff changeset
147 ≈⟨ cdr ( cdr ( assoc )) ⟩
30
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 29
diff changeset
148 ( TMap μ d o ( FMap T h o ( ( TMap μ c o FMap T g ) o f ) ) )
28
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 27
diff changeset
149 ≈⟨ assoc ⟩ --- ( f o ( g o h ) ) = ( ( f o g ) o h )
30
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 29
diff changeset
150 ( ( TMap μ d o FMap T h ) o ( (TMap μ c o FMap T g ) o f ) )
25
8117bafdec7a on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 24
diff changeset
151 ≈⟨ assoc ⟩
30
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 29
diff changeset
152 ( ( ( TMap μ d o FMap T h ) o (TMap μ c o FMap T g ) ) o f )
253
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 153
diff changeset
153 ≈↑⟨ car assoc ⟩
30
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 29
diff changeset
154 ( ( TMap μ d o ( FMap T h o ( TMap μ c o FMap T g ) ) ) o f )
28
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 27
diff changeset
155 ≈⟨ car ( cdr (assoc) ) ⟩
30
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 29
diff changeset
156 ( ( TMap μ d o ( ( FMap T h o TMap μ c ) o FMap T g ) ) o f )
28
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 27
diff changeset
157 ≈⟨ car assoc ⟩
30
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 29
diff changeset
158 ( ( ( TMap μ d o ( FMap T h o TMap μ c ) ) o FMap T g ) o f )
28
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 27
diff changeset
159 ≈⟨ car (car ( cdr ( begin
30
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 29
diff changeset
160 ( FMap T h o TMap μ c )
66
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 63
diff changeset
161 ≈⟨ nat μ ⟩
30
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 29
diff changeset
162 ( TMap μ (FObj T d) o FMap T (FMap T h) )
25
8117bafdec7a on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 24
diff changeset
163
8117bafdec7a on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 24
diff changeset
164 ))) ⟩
30
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 29
diff changeset
165 ( ( ( TMap μ d o ( TMap μ ( FObj T d) o FMap T ( FMap T h ) ) ) o FMap T g ) o f )
253
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 153
diff changeset
166 ≈↑⟨ car assoc ⟩
30
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 29
diff changeset
167 ( ( TMap μ d o ( ( TMap μ ( FObj T d) o FMap T ( FMap T h ) ) o FMap T g ) ) o f )
253
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 153
diff changeset
168 ≈↑⟨ car ( cdr assoc ) ⟩
30
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 29
diff changeset
169 ( ( TMap μ d o ( TMap μ ( FObj T d) o ( FMap T ( FMap T h ) o FMap T g ) ) ) o f )
253
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 153
diff changeset
170 ≈↑⟨ car ( cdr (cdr (distr T ))) ⟩
30
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 29
diff changeset
171 ( ( TMap μ d o ( TMap μ ( FObj T d) o FMap T ( ( FMap T h o g ) ) ) ) o f )
28
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 27
diff changeset
172 ≈⟨ car assoc ⟩
30
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 29
diff changeset
173 ( ( ( TMap μ d o TMap μ ( FObj T d) ) o FMap T ( ( FMap T h o g ) ) ) o f )
28
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 27
diff changeset
174 ≈⟨ car ( car (
27
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 26
diff changeset
175 begin
30
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 29
diff changeset
176 ( TMap μ d o TMap μ (FObj T d) )
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 474
diff changeset
177 ≈⟨ IsMonad.assoc M ⟩
30
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 29
diff changeset
178 ( TMap μ d o FMap T (TMap μ d) )
27
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 26
diff changeset
179
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 26
diff changeset
180 )) ⟩
30
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 29
diff changeset
181 ( ( ( TMap μ d o FMap T ( TMap μ d) ) o FMap T ( ( FMap T h o g ) ) ) o f )
253
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 153
diff changeset
182 ≈↑⟨ car assoc ⟩
30
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 29
diff changeset
183 ( ( TMap μ d o ( FMap T ( TMap μ d ) o FMap T ( ( FMap T h o g ) ) ) ) o f )
253
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 153
diff changeset
184 ≈↑⟨ assoc ⟩
30
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 29
diff changeset
185 ( TMap μ d o ( ( FMap T ( TMap μ d ) o FMap T ( ( FMap T h o g ) ) ) o f ) )
253
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 153
diff changeset
186 ≈↑⟨ cdr ( car ( distr T )) ⟩
30
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 29
diff changeset
187 ( TMap μ d o ( FMap T ( ( ( TMap μ d ) o ( FMap T h o g ) ) ) o f ) )
23
736df1a35807 join assoc on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 22
diff changeset
188 ≈⟨ refl-hom ⟩
130
5f331dfc000b remove Kleisli record
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 108
diff changeset
189 join M ( ( TMap μ d o ( FMap T h o g ) ) ) f
23
736df1a35807 join assoc on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 22
diff changeset
190 ≈⟨ refl-hom ⟩
130
5f331dfc000b remove Kleisli record
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 108
diff changeset
191 join M ( join M h g) f
24
171c31acf78e on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
192 ∎ where open ≈-Reasoning (A)
3
dce706edd66b Kleisli
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 2
diff changeset
193
82
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
194 --
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
195 -- o-resp in Kleisli Category ( for Functor definitions )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
196 --
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
197 Lemma10 : {a b c : Obj A} → (f g : Hom A a (FObj T b) ) → (h i : Hom A b (FObj T c) ) →
130
5f331dfc000b remove Kleisli record
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 108
diff changeset
198 A [ f ≈ g ] → A [ h ≈ i ] → A [ (join M h f) ≈ (join M i g) ]
474
2d32ded94aaf clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 467
diff changeset
199 Lemma10 {a} {b} {c} f g h i f≈g h≈i = let open ≈-Reasoning (A) in
74
49e6eb3ef9c0 Kleisli Category constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
200 begin
130
5f331dfc000b remove Kleisli record
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 108
diff changeset
201 join M h f
74
49e6eb3ef9c0 Kleisli Category constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
202 ≈⟨⟩
49e6eb3ef9c0 Kleisli Category constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
203 TMap μ c o ( FMap T h o f )
474
2d32ded94aaf clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 467
diff changeset
204 ≈⟨ cdr ( car ( fcong T h≈i )) ⟩
2d32ded94aaf clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 467
diff changeset
205 TMap μ c o ( FMap T i o f )
2d32ded94aaf clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 467
diff changeset
206 ≈⟨ cdr ( cdr f≈g ) ⟩
74
49e6eb3ef9c0 Kleisli Category constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
207 TMap μ c o ( FMap T i o g )
49e6eb3ef9c0 Kleisli Category constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
208 ≈⟨⟩
130
5f331dfc000b remove Kleisli record
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 108
diff changeset
209 join M i g
74
49e6eb3ef9c0 Kleisli Category constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
210
49e6eb3ef9c0 Kleisli Category constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
211
82
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
212 --
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
213 -- Hom in Kleisli Category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
214 --
74
49e6eb3ef9c0 Kleisli Category constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
215
87
4690953794c4 MEsolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 86
diff changeset
216
4690953794c4 MEsolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 86
diff changeset
217 record KleisliHom { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } { T : Functor A A } (a : Obj A) (b : Obj A)
467
ba042c2d3ff5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
218 : Set c₂ where
ba042c2d3ff5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
219 field
ba042c2d3ff5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
220 KMap : Hom A a ( FObj T b )
ba042c2d3ff5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
221
ba042c2d3ff5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
222 open KleisliHom
69
84a150c980ce generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 68
diff changeset
223
467
ba042c2d3ff5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
224 -- we need this to make agda check stop
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
225 KHom = λ (a b : Obj A) → KleisliHom {c₁} {c₂} {ℓ} {A} {T} a b
87
4690953794c4 MEsolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 86
diff changeset
226
72
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 71
diff changeset
227 K-id : {a : Obj A} → KHom a a
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 71
diff changeset
228 K-id {a = a} = record { KMap = TMap η a }
56
83ff8d48fdca add unitility
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 31
diff changeset
229
69
84a150c980ce generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 68
diff changeset
230 open import Relation.Binary.Core
56
83ff8d48fdca add unitility
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 31
diff changeset
231
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
232 _⋍_ : { a : Obj A } { b : Obj A } (f g : KHom a b ) → Set ℓ
73
b75b5792bd81 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 72
diff changeset
233 _⋍_ {a} {b} f g = A [ KMap f ≈ KMap g ]
71
709c1bde54dc Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
234
108
e763efd30868 on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 97
diff changeset
235 _*_ : { a b c : Obj A } → ( KHom b c) → ( KHom a b) → KHom a c
130
5f331dfc000b remove Kleisli record
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 108
diff changeset
236 _*_ {a} {b} {c} g f = record { KMap = join M {a} {b} {c} (KMap g) (KMap f) }
70
fb3c48b375b3 Kleisli Category ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
237
72
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 71
diff changeset
238 isKleisliCategory : IsCategory ( Obj A ) KHom _⋍_ _*_ K-id
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 71
diff changeset
239 isKleisliCategory = record { isEquivalence = isEquivalence
71
709c1bde54dc Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
240 ; identityL = KidL
709c1bde54dc Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
241 ; identityR = KidR
709c1bde54dc Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
242 ; o-resp-≈ = Ko-resp
709c1bde54dc Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
243 ; associative = Kassoc
69
84a150c980ce generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 68
diff changeset
244 }
84a150c980ce generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 68
diff changeset
245 where
73
b75b5792bd81 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 72
diff changeset
246 open ≈-Reasoning (A)
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
247 isEquivalence : { a b : Obj A } →
72
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 71
diff changeset
248 IsEquivalence {_} {_} {KHom a b} _⋍_
82
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
249 isEquivalence {C} {D} = -- this is the same function as A's equivalence but has different types
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
250 record { refl = refl-hom
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
251 ; sym = sym
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
252 ; trans = trans-hom
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
253 }
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
254 KidL : {C D : Obj A} → {f : KHom C D} → (K-id * f) ⋍ f
73
b75b5792bd81 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 72
diff changeset
255 KidL {_} {_} {f} = Lemma7 (KMap f)
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
256 KidR : {C D : Obj A} → {f : KHom C D} → (f * K-id) ⋍ f
73
b75b5792bd81 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 72
diff changeset
257 KidR {_} {_} {f} = Lemma8 (KMap f)
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
258 Ko-resp : {a b c : Obj A} → {f g : KHom a b } → {h i : KHom b c } →
71
709c1bde54dc Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
259 f ⋍ g → h ⋍ i → (h * f) ⋍ (i * g)
74
49e6eb3ef9c0 Kleisli Category constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
260 Ko-resp {a} {b} {c} {f} {g} {h} {i} eq-fg eq-hi = Lemma10 {a} {b} {c} (KMap f) (KMap g) (KMap h) (KMap i) eq-fg eq-hi
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
261 Kassoc : {a b c d : Obj A} → {f : KHom c d } → {g : KHom b c } → {h : KHom a b } →
71
709c1bde54dc Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
262 (f * (g * h)) ⋍ ((f * g) * h)
73
b75b5792bd81 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 72
diff changeset
263 Kassoc {_} {_} {_} {_} {f} {g} {h} = Lemma9 (KMap f) (KMap g) (KMap h)
3
dce706edd66b Kleisli
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 2
diff changeset
264
78
b3c023f7c929 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 77
diff changeset
265 KleisliCategory : Category c₁ c₂ ℓ
75
8e665152c306 Comparison Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
266 KleisliCategory =
8e665152c306 Comparison Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
267 record { Obj = Obj A
8e665152c306 Comparison Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
268 ; Hom = KHom
8e665152c306 Comparison Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
269 ; _o_ = _*_
8e665152c306 Comparison Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
270 ; _≈_ = _⋍_
8e665152c306 Comparison Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
271 ; Id = K-id
8e665152c306 Comparison Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
272 ; isCategory = isKleisliCategory
8e665152c306 Comparison Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
273 }
56
83ff8d48fdca add unitility
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 31
diff changeset
274
82
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
275 --
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
276 -- Resolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
277 -- T = U_T U_F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
278 -- nat-ε
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
279 -- nat-η
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
280 --
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
281
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
282 ufmap : {a b : Obj A} (f : KHom a b ) → Hom A (FObj T a) (FObj T b)
80
e945c201364a Adjoint of U_T F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 79
diff changeset
283 ufmap {a} {b} f = A [ TMap μ (b) o FMap T (KMap f) ]
e945c201364a Adjoint of U_T F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 79
diff changeset
284
75
8e665152c306 Comparison Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
285 U_T : Functor KleisliCategory A
8e665152c306 Comparison Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
286 U_T = record {
8e665152c306 Comparison Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
287 FObj = FObj T
8e665152c306 Comparison Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
288 ; FMap = ufmap
8e665152c306 Comparison Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
289 ; isFunctor = record
8e665152c306 Comparison Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
290 { ≈-cong = ≈-cong
8e665152c306 Comparison Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
291 ; identity = identity
76
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
292 ; distr = distr1
75
8e665152c306 Comparison Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
293 }
8e665152c306 Comparison Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
294 } where
8e665152c306 Comparison Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
295 identity : {a : Obj A} → A [ ufmap (K-id {a}) ≈ id1 A (FObj T a) ]
8e665152c306 Comparison Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
296 identity {a} = let open ≈-Reasoning (A) in
8e665152c306 Comparison Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
297 begin
8e665152c306 Comparison Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
298 TMap μ (a) o FMap T (TMap η a)
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 474
diff changeset
299 ≈⟨ IsMonad.unity2 M ⟩
253
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 153
diff changeset
300 id (FObj T a)
75
8e665152c306 Comparison Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
301
8e665152c306 Comparison Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
302 ≈-cong : {a b : Obj A} {f g : KHom a b} → A [ KMap f ≈ KMap g ] → A [ ufmap f ≈ ufmap g ]
8e665152c306 Comparison Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
303 ≈-cong {a} {b} {f} {g} f≈g = let open ≈-Reasoning (A) in
8e665152c306 Comparison Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
304 begin
8e665152c306 Comparison Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
305 TMap μ (b) o FMap T (KMap f)
8e665152c306 Comparison Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
306 ≈⟨ cdr (fcong T f≈g) ⟩
8e665152c306 Comparison Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
307 TMap μ (b) o FMap T (KMap g)
8e665152c306 Comparison Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
308
76
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
309 distr1 : {a b c : Obj A} {f : KHom a b} {g : KHom b c} → A [ ufmap (g * f) ≈ (A [ ufmap g o ufmap f ] )]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
310 distr1 {a} {b} {c} {f} {g} = let open ≈-Reasoning (A) in
75
8e665152c306 Comparison Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
311 begin
8e665152c306 Comparison Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
312 ufmap (g * f)
76
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
313 ≈⟨⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
314 ufmap {a} {c} ( record { KMap = TMap μ (c) o (FMap T (KMap g) o (KMap f)) } )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
315 ≈⟨⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
316 TMap μ (c) o FMap T ( TMap μ (c) o (FMap T (KMap g) o (KMap f)))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
317 ≈⟨ cdr ( distr T) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
318 TMap μ (c) o (( FMap T ( TMap μ (c)) o FMap T (FMap T (KMap g) o (KMap f))))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
319 ≈⟨ assoc ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
320 (TMap μ (c) o ( FMap T ( TMap μ (c)))) o FMap T (FMap T (KMap g) o (KMap f))
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 474
diff changeset
321 ≈⟨ car (sym (IsMonad.assoc M)) ⟩
76
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
322 (TMap μ (c) o ( TMap μ (FObj T c))) o FMap T (FMap T (KMap g) o (KMap f))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
323 ≈⟨ sym assoc ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
324 TMap μ (c) o (( TMap μ (FObj T c)) o FMap T (FMap T (KMap g) o (KMap f)))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
325 ≈⟨ cdr (cdr (distr T)) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
326 TMap μ (c) o (( TMap μ (FObj T c)) o (FMap T (FMap T (KMap g)) o FMap T (KMap f)))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
327 ≈⟨ cdr (assoc) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
328 TMap μ (c) o ((( TMap μ (FObj T c)) o (FMap T (FMap T (KMap g)))) o FMap T (KMap f))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
329 ≈⟨ sym (cdr (car (nat μ ))) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
330 TMap μ (c) o ((FMap T (KMap g ) o TMap μ (b)) o FMap T (KMap f ))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
331 ≈⟨ cdr (sym assoc) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
332 TMap μ (c) o (FMap T (KMap g ) o ( TMap μ (b) o FMap T (KMap f )))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
333 ≈⟨ assoc ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
334 ( TMap μ (c) o FMap T (KMap g ) ) o ( TMap μ (b) o FMap T (KMap f ) )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
335 ≈⟨⟩
75
8e665152c306 Comparison Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
336 ufmap g o ufmap f
8e665152c306 Comparison Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
337
8e665152c306 Comparison Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
338
8e665152c306 Comparison Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
339
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
340 ffmap : {a b : Obj A} (f : Hom A a b) → KHom a b
474
2d32ded94aaf clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 467
diff changeset
341 ffmap {a} {b} f = record { KMap = A [ TMap η b o f ] }
75
8e665152c306 Comparison Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
342
8e665152c306 Comparison Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
343 F_T : Functor A KleisliCategory
8e665152c306 Comparison Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
344 F_T = record {
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
345 FObj = λ a → a
75
8e665152c306 Comparison Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
346 ; FMap = ffmap
8e665152c306 Comparison Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
347 ; isFunctor = record
8e665152c306 Comparison Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
348 { ≈-cong = ≈-cong
8e665152c306 Comparison Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
349 ; identity = identity
76
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
350 ; distr = distr1
75
8e665152c306 Comparison Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
351 }
8e665152c306 Comparison Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
352 } where
8e665152c306 Comparison Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
353 identity : {a : Obj A} → A [ A [ TMap η a o id1 A a ] ≈ TMap η a ]
8e665152c306 Comparison Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
354 identity {a} = IsCategory.identityR ( Category.isCategory A)
82
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
355 -- Category.cod A f and Category.cod A g are actualy the same b, so we don't need cong-≈, just refl
474
2d32ded94aaf clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 467
diff changeset
356 lemma1 : {b : Obj A} → A [ TMap η b ≈ TMap η b ]
2d32ded94aaf clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 467
diff changeset
357 lemma1 = IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory A ))
2d32ded94aaf clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 467
diff changeset
358 ≈-cong : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → A [ A [ TMap η b o f ] ≈ A [ TMap η b o g ] ]
2d32ded94aaf clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 467
diff changeset
359 ≈-cong f≈g = (IsCategory.o-resp-≈ (Category.isCategory A)) f≈g lemma1
76
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
360 distr1 : {a b c : Obj A} {f : Hom A a b} {g : Hom A b c} →
75
8e665152c306 Comparison Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
361 ( ffmap (A [ g o f ]) ⋍ ( ffmap g * ffmap f ) )
77
528c7e27af91 Resolution U_T, F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 76
diff changeset
362 distr1 {a} {b} {c} {f} {g} = let open ≈-Reasoning (A) in
75
8e665152c306 Comparison Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
363 begin
8e665152c306 Comparison Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
364 KMap (ffmap (A [ g o f ]))
77
528c7e27af91 Resolution U_T, F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 76
diff changeset
365 ≈⟨⟩
528c7e27af91 Resolution U_T, F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 76
diff changeset
366 TMap η (c) o (g o f)
528c7e27af91 Resolution U_T, F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 76
diff changeset
367 ≈⟨ assoc ⟩
528c7e27af91 Resolution U_T, F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 76
diff changeset
368 (TMap η (c) o g) o f
528c7e27af91 Resolution U_T, F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 76
diff changeset
369 ≈⟨ car (sym (nat η)) ⟩
528c7e27af91 Resolution U_T, F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 76
diff changeset
370 (FMap T g o TMap η (b)) o f
528c7e27af91 Resolution U_T, F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 76
diff changeset
371 ≈⟨ sym idL ⟩
253
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 153
diff changeset
372 id (FObj T c) o ((FMap T g o TMap η (b)) o f)
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 474
diff changeset
373 ≈⟨ sym (car (IsMonad.unity2 M)) ⟩
77
528c7e27af91 Resolution U_T, F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 76
diff changeset
374 (TMap μ c o FMap T (TMap η c)) o ((FMap T g o TMap η (b)) o f)
528c7e27af91 Resolution U_T, F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 76
diff changeset
375 ≈⟨ sym assoc ⟩
528c7e27af91 Resolution U_T, F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 76
diff changeset
376 TMap μ c o ( FMap T (TMap η c) o ((FMap T g o TMap η (b)) o f) )
528c7e27af91 Resolution U_T, F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 76
diff changeset
377 ≈⟨ cdr (cdr (sym assoc)) ⟩
528c7e27af91 Resolution U_T, F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 76
diff changeset
378 TMap μ c o ( FMap T (TMap η c) o (FMap T g o (TMap η (b) o f)))
528c7e27af91 Resolution U_T, F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 76
diff changeset
379 ≈⟨ cdr assoc ⟩
528c7e27af91 Resolution U_T, F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 76
diff changeset
380 TMap μ c o ( ( FMap T (TMap η c) o FMap T g ) o (TMap η (b) o f) )
528c7e27af91 Resolution U_T, F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 76
diff changeset
381 ≈⟨ sym (cdr ( car ( distr T ))) ⟩
528c7e27af91 Resolution U_T, F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 76
diff changeset
382 TMap μ c o ( ( FMap T (TMap η c o g)) o (TMap η (b) o f))
528c7e27af91 Resolution U_T, F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 76
diff changeset
383 ≈⟨ assoc ⟩
528c7e27af91 Resolution U_T, F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 76
diff changeset
384 (TMap μ c o ( FMap T (TMap η c o g))) o (TMap η (b) o f)
528c7e27af91 Resolution U_T, F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 76
diff changeset
385 ≈⟨ assoc ⟩
528c7e27af91 Resolution U_T, F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 76
diff changeset
386 ((TMap μ c o (FMap T (TMap η c o g))) o TMap η b) o f
528c7e27af91 Resolution U_T, F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 76
diff changeset
387 ≈⟨ sym assoc ⟩
528c7e27af91 Resolution U_T, F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 76
diff changeset
388 (TMap μ c o (FMap T (TMap η c o g))) o (TMap η b o f)
528c7e27af91 Resolution U_T, F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 76
diff changeset
389 ≈⟨ sym assoc ⟩
528c7e27af91 Resolution U_T, F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 76
diff changeset
390 TMap μ c o ( (FMap T (TMap η c o g)) o (TMap η b o f) )
528c7e27af91 Resolution U_T, F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 76
diff changeset
391 ≈⟨⟩
130
5f331dfc000b remove Kleisli record
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 108
diff changeset
392 join M (TMap η c o g) (TMap η b o f)
77
528c7e27af91 Resolution U_T, F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 76
diff changeset
393 ≈⟨⟩
75
8e665152c306 Comparison Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
394 KMap ( ffmap g * ffmap f )
8e665152c306 Comparison Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
395
8e665152c306 Comparison Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
396
82
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
397 --
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
398 -- T = (U_T ○ F_T)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
399 --
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
400
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
401 Lemma11-1 : ∀{a b : Obj A} → (f : Hom A a b ) → A [ FMap T f ≈ FMap (U_T ○ F_T) f ]
79
84723389e3c9 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 78
diff changeset
402 Lemma11-1 {a} {b} f = let open ≈-Reasoning (A) in
84723389e3c9 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 78
diff changeset
403 sym ( begin
84723389e3c9 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 78
diff changeset
404 FMap (U_T ○ F_T) f
84723389e3c9 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 78
diff changeset
405 ≈⟨⟩
84723389e3c9 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 78
diff changeset
406 FMap U_T ( FMap F_T f )
84723389e3c9 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 78
diff changeset
407 ≈⟨⟩
84723389e3c9 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 78
diff changeset
408 TMap μ (b) o FMap T (KMap ( ffmap f ) )
84723389e3c9 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 78
diff changeset
409 ≈⟨⟩
84723389e3c9 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 78
diff changeset
410 TMap μ (b) o FMap T (TMap η (b) o f)
84723389e3c9 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 78
diff changeset
411 ≈⟨ cdr (distr T ) ⟩
84723389e3c9 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 78
diff changeset
412 TMap μ (b) o ( FMap T (TMap η (b)) o FMap T f)
84723389e3c9 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 78
diff changeset
413 ≈⟨ assoc ⟩
84723389e3c9 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 78
diff changeset
414 (TMap μ (b) o FMap T (TMap η (b))) o FMap T f
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 474
diff changeset
415 ≈⟨ car (IsMonad.unity2 M) ⟩
253
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 153
diff changeset
416 id (FObj T b) o FMap T f
79
84723389e3c9 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 78
diff changeset
417 ≈⟨ idL ⟩
84723389e3c9 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 78
diff changeset
418 FMap T f
84723389e3c9 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 78
diff changeset
419 ∎ )
84723389e3c9 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 78
diff changeset
420
82
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
421 -- construct ≃
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
422
81
0404b2ba7db6 Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 80
diff changeset
423 Lemma11 : T ≃ (U_T ○ F_T)
0404b2ba7db6 Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 80
diff changeset
424 Lemma11 f = Category.Cat.refl (Lemma11-1 f)
78
b3c023f7c929 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 77
diff changeset
425
82
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
426 --
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
427 -- natural transformations
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
428 --
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
429
78
b3c023f7c929 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 77
diff changeset
430 nat-η : NTrans A A identityFunctor ( U_T ○ F_T )
467
ba042c2d3ff5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
431 nat-η = record { TMap = λ x → TMap η x ; isNTrans = record { commute = commute } } where
ba042c2d3ff5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
432 commute : {a b : Obj A} {f : Hom A a b}
79
84723389e3c9 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 78
diff changeset
433 → 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: 300
diff changeset
434 commute {a} {b} {f} = let open ≈-Reasoning (A) in
79
84723389e3c9 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 78
diff changeset
435 begin
84723389e3c9 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 78
diff changeset
436 ( FMap ( U_T ○ F_T ) f ) o ( TMap η a )
84
ee25f96ee8cc record Resolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 83
diff changeset
437 ≈⟨ sym (resp refl-hom (Lemma11-1 f)) ⟩
ee25f96ee8cc record Resolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 83
diff changeset
438 FMap T f o TMap η a
79
84723389e3c9 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 78
diff changeset
439 ≈⟨ nat η ⟩
84
ee25f96ee8cc record Resolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 83
diff changeset
440 TMap η b o f
79
84723389e3c9 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 78
diff changeset
441
77
528c7e27af91 Resolution U_T, F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 76
diff changeset
442
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
443 tmap-ε : (a : Obj A) → KHom (FObj T a) a
78
b3c023f7c929 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 77
diff changeset
444 tmap-ε a = record { KMap = id1 A (FObj T a) }
b3c023f7c929 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 77
diff changeset
445
b3c023f7c929 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 77
diff changeset
446 nat-ε : NTrans KleisliCategory KleisliCategory ( F_T ○ U_T ) identityFunctor
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
447 nat-ε = record { TMap = λ a → tmap-ε a; isNTrans = isNTrans1 } where
130
5f331dfc000b remove Kleisli record
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 108
diff changeset
448 commute1 : {a b : Obj A} {f : KHom a b}
78
b3c023f7c929 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 77
diff changeset
449 → (f * ( tmap-ε a ) ) ⋍ (( tmap-ε b ) * ( FMap (F_T ○ U_T) f ) )
130
5f331dfc000b remove Kleisli record
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 108
diff changeset
450 commute1 {a} {b} {f} = let open ≈-Reasoning (A) in
79
84723389e3c9 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 78
diff changeset
451 sym ( begin
84723389e3c9 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 78
diff changeset
452 KMap (( tmap-ε b ) * ( FMap (F_T ○ U_T) f ))
80
e945c201364a Adjoint of U_T F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 79
diff changeset
453 ≈⟨⟩
253
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 153
diff changeset
454 TMap μ b o ( FMap T ( id (FObj T b) ) o ( KMap (FMap (F_T ○ U_T) f ) ))
80
e945c201364a Adjoint of U_T F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 79
diff changeset
455 ≈⟨ cdr ( cdr (
e945c201364a Adjoint of U_T F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 79
diff changeset
456 begin
e945c201364a Adjoint of U_T F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 79
diff changeset
457 KMap (FMap (F_T ○ U_T) f )
e945c201364a Adjoint of U_T F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 79
diff changeset
458 ≈⟨⟩
e945c201364a Adjoint of U_T F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 79
diff changeset
459 KMap (FMap F_T (FMap U_T f))
e945c201364a Adjoint of U_T F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 79
diff changeset
460 ≈⟨⟩
e945c201364a Adjoint of U_T F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 79
diff changeset
461 TMap η (FObj T b) o (TMap μ (b) o FMap T (KMap f))
e945c201364a Adjoint of U_T F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 79
diff changeset
462
e945c201364a Adjoint of U_T F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 79
diff changeset
463 )) ⟩
253
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 153
diff changeset
464 TMap μ b o ( FMap T ( id (FObj T b) ) o (TMap η (FObj T b) o (TMap μ (b) o FMap T (KMap f))))
80
e945c201364a Adjoint of U_T F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 79
diff changeset
465 ≈⟨ cdr (car (IsFunctor.identity (isFunctor T))) ⟩
253
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 153
diff changeset
466 TMap μ b o ( id (FObj T (FObj T b) ) o (TMap η (FObj T b) o (TMap μ (b) o FMap T (KMap f))))
80
e945c201364a Adjoint of U_T F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 79
diff changeset
467 ≈⟨ cdr idL ⟩
e945c201364a Adjoint of U_T F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 79
diff changeset
468 TMap μ b o (TMap η (FObj T b) o (TMap μ (b) o FMap T (KMap f)))
e945c201364a Adjoint of U_T F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 79
diff changeset
469 ≈⟨ assoc ⟩
e945c201364a Adjoint of U_T F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 79
diff changeset
470 (TMap μ b o (TMap η (FObj T b))) o (TMap μ (b) o FMap T (KMap f))
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 474
diff changeset
471 ≈⟨ (car (IsMonad.unity1 M)) ⟩
253
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 153
diff changeset
472 id (FObj T b) o (TMap μ (b) o FMap T (KMap f))
80
e945c201364a Adjoint of U_T F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 79
diff changeset
473 ≈⟨ idL ⟩
e945c201364a Adjoint of U_T F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 79
diff changeset
474 TMap μ b o FMap T (KMap f)
e945c201364a Adjoint of U_T F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 79
diff changeset
475 ≈⟨ cdr (sym idR) ⟩
253
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 153
diff changeset
476 TMap μ b o ( FMap T (KMap f) o id (FObj T a) )
80
e945c201364a Adjoint of U_T F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 79
diff changeset
477 ≈⟨⟩
79
84723389e3c9 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 78
diff changeset
478 KMap (f * ( tmap-ε a ))
84723389e3c9 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 78
diff changeset
479 ∎ )
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
480 isNTrans1 : IsNTrans KleisliCategory KleisliCategory ( F_T ○ U_T ) identityFunctor (λ a → tmap-ε a )
130
5f331dfc000b remove Kleisli record
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 108
diff changeset
481 isNTrans1 = record { commute = commute1 }
77
528c7e27af91 Resolution U_T, F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 76
diff changeset
482
82
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
483 --
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
484 -- μ = U_T ε U_F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
485 --
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
486 tmap-μ : (a : Obj A) → Hom A (FObj ( U_T ○ F_T ) (FObj ( U_T ○ F_T ) a)) (FObj ( U_T ○ F_T ) a)
95
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 94
diff changeset
487 tmap-μ a = FMap U_T ( TMap nat-ε ( FObj F_T a ))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 94
diff changeset
488
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 94
diff changeset
489 nat-μ : NTrans A A (( U_T ○ F_T ) ○ ( U_T ○ F_T )) ( U_T ○ F_T )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 94
diff changeset
490 nat-μ = record { TMap = tmap-μ ; isNTrans = isNTrans1 } where
130
5f331dfc000b remove Kleisli record
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 108
diff changeset
491 commute1 : {a b : Obj A} {f : Hom A a b}
95
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 94
diff changeset
492 → A [ A [ (FMap (U_T ○ F_T) f) o ( tmap-μ a) ] ≈ A [ ( tmap-μ 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: 108
diff changeset
493 commute1 {a} {b} {f} = let open ≈-Reasoning (A) in
95
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 94
diff changeset
494 sym ( begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 94
diff changeset
495 ( tmap-μ b ) o FMap (U_T ○ F_T) ( FMap (U_T ○ F_T) f)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 94
diff changeset
496 ≈⟨⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 94
diff changeset
497 ( FMap U_T ( TMap nat-ε ( 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: 94
diff changeset
498 ≈⟨ sym ( distr U_T) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 94
diff changeset
499 FMap U_T ( KleisliCategory [ TMap nat-ε ( FObj F_T b ) o FMap F_T ( FMap (U_T ○ F_T) f) ] )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 94
diff changeset
500 ≈⟨ fcong U_T (sym (nat nat-ε)) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 94
diff changeset
501 FMap U_T ( KleisliCategory [ (FMap F_T f) o TMap nat-ε ( FObj F_T a ) ] )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 94
diff changeset
502 ≈⟨ distr U_T ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 94
diff changeset
503 (FMap U_T (FMap F_T f)) o FMap U_T ( TMap nat-ε ( FObj F_T a ))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 94
diff changeset
504 ≈⟨⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 94
diff changeset
505 (FMap (U_T ○ F_T) f) o ( tmap-μ a)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 94
diff changeset
506 ∎ )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 94
diff changeset
507 isNTrans1 : IsNTrans A A (( U_T ○ F_T ) ○ ( U_T ○ F_T )) ( U_T ○ F_T ) tmap-μ
130
5f331dfc000b remove Kleisli record
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 108
diff changeset
508 isNTrans1 = record { commute = commute1 }
95
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 94
diff changeset
509
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
510 Lemma12 : {x : Obj A } → A [ TMap nat-μ x ≈ FMap U_T ( TMap nat-ε ( FObj F_T x ) ) ]
80
e945c201364a Adjoint of U_T F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 79
diff changeset
511 Lemma12 {x} = let open ≈-Reasoning (A) in
e945c201364a Adjoint of U_T F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 79
diff changeset
512 sym ( begin
e945c201364a Adjoint of U_T F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 79
diff changeset
513 FMap U_T ( TMap nat-ε ( FObj F_T x ) )
e945c201364a Adjoint of U_T F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 79
diff changeset
514 ≈⟨⟩
95
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 94
diff changeset
515 tmap-μ x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 94
diff changeset
516 ≈⟨⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 94
diff changeset
517 TMap nat-μ x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 94
diff changeset
518 ∎ )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 94
diff changeset
519
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
520 Lemma13 : {x : Obj A } → A [ TMap μ x ≈ FMap U_T ( TMap nat-ε ( FObj F_T x ) ) ]
95
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 94
diff changeset
521 Lemma13 {x} = let open ≈-Reasoning (A) in
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 94
diff changeset
522 sym ( begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 94
diff changeset
523 FMap U_T ( TMap nat-ε ( FObj F_T x ) )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 94
diff changeset
524 ≈⟨⟩
253
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 153
diff changeset
525 TMap μ x o FMap T (id (FObj T x) )
80
e945c201364a Adjoint of U_T F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 79
diff changeset
526 ≈⟨ cdr (IsFunctor.identity (isFunctor T)) ⟩
253
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 153
diff changeset
527 TMap μ x o id (FObj T (FObj T x) )
80
e945c201364a Adjoint of U_T F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 79
diff changeset
528 ≈⟨ idR ⟩
e945c201364a Adjoint of U_T F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 79
diff changeset
529 TMap μ x
e945c201364a Adjoint of U_T F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 79
diff changeset
530 ∎ )
78
b3c023f7c929 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 77
diff changeset
531
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 474
diff changeset
532 Adj_T : Adjunction A KleisliCategory
84
ee25f96ee8cc record Resolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 83
diff changeset
533 Adj_T = record {
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 474
diff changeset
534 U = U_T ;
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 474
diff changeset
535 F = F_T ;
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 474
diff changeset
536 η = nat-η ;
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 474
diff changeset
537 ε = nat-ε ;
80
e945c201364a Adjoint of U_T F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 79
diff changeset
538 isAdjunction = record {
e945c201364a Adjoint of U_T F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 79
diff changeset
539 adjoint1 = adjoint1 ;
e945c201364a Adjoint of U_T F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 79
diff changeset
540 adjoint2 = adjoint2
e945c201364a Adjoint of U_T F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 79
diff changeset
541 }
e945c201364a Adjoint of U_T F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 79
diff changeset
542 } where
e945c201364a Adjoint of U_T F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 79
diff changeset
543 adjoint1 : { b : Obj KleisliCategory } →
e945c201364a Adjoint of U_T F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 79
diff changeset
544 A [ A [ ( FMap U_T ( TMap nat-ε b)) o ( TMap nat-η ( FObj U_T b )) ] ≈ id1 A (FObj U_T b) ]
81
0404b2ba7db6 Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 80
diff changeset
545 adjoint1 {b} = let open ≈-Reasoning (A) in
0404b2ba7db6 Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 80
diff changeset
546 begin
0404b2ba7db6 Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 80
diff changeset
547 ( FMap U_T ( TMap nat-ε b)) o ( TMap nat-η ( FObj U_T b ))
0404b2ba7db6 Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 80
diff changeset
548 ≈⟨⟩
253
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 153
diff changeset
549 (TMap μ (b) o FMap T (id (FObj T b ))) o ( TMap η ( FObj T b ))
81
0404b2ba7db6 Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 80
diff changeset
550 ≈⟨ car ( cdr (IsFunctor.identity (isFunctor T))) ⟩
253
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 153
diff changeset
551 (TMap μ (b) o (id (FObj T (FObj T b )))) o ( TMap η ( FObj T b ))
81
0404b2ba7db6 Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 80
diff changeset
552 ≈⟨ car idR ⟩
0404b2ba7db6 Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 80
diff changeset
553 TMap μ (b) o ( TMap η ( FObj T b ))
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 474
diff changeset
554 ≈⟨ IsMonad.unity1 M ⟩
253
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 153
diff changeset
555 id (FObj U_T b)
81
0404b2ba7db6 Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 80
diff changeset
556
80
e945c201364a Adjoint of U_T F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 79
diff changeset
557 adjoint2 : {a : Obj A} →
e945c201364a Adjoint of U_T F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 79
diff changeset
558 KleisliCategory [ KleisliCategory [ ( TMap nat-ε ( FObj F_T a )) o ( FMap F_T ( TMap nat-η a )) ]
87
4690953794c4 MEsolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 86
diff changeset
559 ≈ id1 KleisliCategory (FObj F_T a) ]
81
0404b2ba7db6 Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 80
diff changeset
560 adjoint2 {a} = let open ≈-Reasoning (A) in
0404b2ba7db6 Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 80
diff changeset
561 begin
0404b2ba7db6 Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 80
diff changeset
562 KMap (( TMap nat-ε ( FObj F_T a )) * ( FMap F_T ( TMap nat-η a )) )
0404b2ba7db6 Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 80
diff changeset
563 ≈⟨⟩
253
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 153
diff changeset
564 TMap μ a o (FMap T (id (FObj T a) ) o ((TMap η (FObj T a)) o (TMap η a)))
81
0404b2ba7db6 Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 80
diff changeset
565 ≈⟨ cdr ( car ( IsFunctor.identity (isFunctor T))) ⟩
253
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 153
diff changeset
566 TMap μ a o ((id (FObj T (FObj T a) )) o ((TMap η (FObj T a)) o (TMap η a)))
81
0404b2ba7db6 Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 80
diff changeset
567 ≈⟨ cdr ( idL ) ⟩
0404b2ba7db6 Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 80
diff changeset
568 TMap μ a o ((TMap η (FObj T a)) o (TMap η a))
0404b2ba7db6 Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 80
diff changeset
569 ≈⟨ assoc ⟩
0404b2ba7db6 Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 80
diff changeset
570 (TMap μ a o (TMap η (FObj T a))) o (TMap η a)
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 474
diff changeset
571 ≈⟨ car (IsMonad.unity1 M) ⟩
253
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 153
diff changeset
572 id (FObj T a) o (TMap η a)
81
0404b2ba7db6 Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 80
diff changeset
573 ≈⟨ idL ⟩
0404b2ba7db6 Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 80
diff changeset
574 TMap η a
0404b2ba7db6 Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 80
diff changeset
575 ≈⟨⟩
0404b2ba7db6 Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 80
diff changeset
576 TMap η (FObj F_T a)
0404b2ba7db6 Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 80
diff changeset
577 ≈⟨⟩
0404b2ba7db6 Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 80
diff changeset
578 KMap (id1 KleisliCategory (FObj F_T a))
82
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
579
77
528c7e27af91 Resolution U_T, F_T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 76
diff changeset
580
87
4690953794c4 MEsolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 86
diff changeset
581 open MResolution
84
ee25f96ee8cc record Resolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 83
diff changeset
582
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 474
diff changeset
583 Resolution_T : MResolution A KleisliCategory ( record { T = T ; η = η ; μ = μ; isMonad = M } )
84
ee25f96ee8cc record Resolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 83
diff changeset
584 Resolution_T = record {
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 474
diff changeset
585 UR = U_T ;
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 474
diff changeset
586 FR = F_T ;
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 474
diff changeset
587 ηR = nat-η ;
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 474
diff changeset
588 εR = nat-ε ;
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 474
diff changeset
589 μR = nat-μ ;
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 474
diff changeset
590 Adj = Adjunction.isAdjunction Adj_T ;
87
4690953794c4 MEsolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 86
diff changeset
591 T=UF = Lemma11;
4690953794c4 MEsolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 86
diff changeset
592 μ=UεF = Lemma12
84
ee25f96ee8cc record Resolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 83
diff changeset
593 }
ee25f96ee8cc record Resolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 83
diff changeset
594
97
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 96
diff changeset
595 -- end