|
0
|
1 module nat where
|
|
|
2
|
|
|
3 -- Monad
|
|
|
4 -- Category A
|
|
|
5 -- A = Category
|
|
|
6 -- Functor T : A -> A
|
|
|
7 --T(a) = t(a)
|
|
|
8 --T(f) = tf(f)
|
|
|
9
|
|
2
|
10 open import Category -- https://github.com/konn/category-agda
|
|
0
|
11 open import Level
|
|
|
12 open Functor
|
|
|
13
|
|
1
|
14 --T(g f) = T(g) T(f)
|
|
|
15
|
|
0
|
16 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 }
|
|
|
17 -> A [ ( FMap T (A [ g o f ] )) ≈ (A [ FMap T g o FMap T f ]) ]
|
|
|
18 Lemma1 = \t -> IsFunctor.distr ( isFunctor t )
|
|
|
19
|
|
|
20 -- F(f)
|
|
|
21 -- F(a) ----> F(b)
|
|
|
22 -- | |
|
|
|
23 -- |t(a) |t(b) G(f)t(a) = t(b)F(f)
|
|
|
24 -- | |
|
|
|
25 -- v v
|
|
|
26 -- G(a) ----> G(b)
|
|
|
27 -- G(f)
|
|
|
28
|
|
7
|
29 record IsNTrans {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (D : Category c₁ c₂ ℓ) (C : Category c₁′ c₂′ ℓ′)
|
|
0
|
30 ( F G : Functor D C )
|
|
7
|
31 (Trans : (A : Obj D) → Hom C (FObj F A) (FObj G A))
|
|
0
|
32 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where
|
|
|
33 field
|
|
|
34 naturality : {a b : Obj D} {f : Hom D a b}
|
|
7
|
35 → C [ C [ ( FMap G f ) o ( Trans a ) ] ≈ C [ (Trans b ) o (FMap F f) ] ]
|
|
0
|
36 -- uniqness : {d : Obj D}
|
|
7
|
37 -- → C [ Trans d ≈ Trans d ]
|
|
0
|
38
|
|
|
39
|
|
7
|
40 record NTrans {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (domain : Category c₁ c₂ ℓ) (codomain : Category c₁′ c₂′ ℓ′) (F G : Functor domain codomain )
|
|
0
|
41 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where
|
|
|
42 field
|
|
7
|
43 Trans : (A : Obj domain) → Hom codomain (FObj F A) (FObj G A)
|
|
|
44 isNTrans : IsNTrans domain codomain F G Trans
|
|
0
|
45
|
|
7
|
46 open NTrans
|
|
1
|
47 Lemma2 : {c₁ c₂ l : Level} {A : Category c₁ c₂ l} {F G : Functor A A}
|
|
7
|
48 -> (μ : NTrans A A F G) -> {a b : Obj A} { f : Hom A a b }
|
|
|
49 -> A [ A [ FMap G f o Trans μ a ] ≈ A [ Trans μ b o FMap F f ] ]
|
|
|
50 Lemma2 = \n -> IsNTrans.naturality ( isNTrans n )
|
|
0
|
51
|
|
|
52 open import Category.Cat
|
|
|
53
|
|
|
54 -- η : 1_A -> T
|
|
|
55 -- μ : TT -> T
|
|
|
56 -- μ(a)η(T(a)) = a
|
|
|
57 -- μ(a)T(η(a)) = a
|
|
|
58 -- μ(a)(μ(T(a))) = μ(a)T(μ(a))
|
|
|
59
|
|
1
|
60 record IsMonad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
|
|
|
61 ( T : Functor A A )
|
|
7
|
62 ( η : NTrans A A identityFunctor T )
|
|
|
63 ( μ : NTrans A A (T ○ T) T)
|
|
1
|
64 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
|
|
|
65 field
|
|
7
|
66 assoc : {a : Obj A} -> A [ A [ Trans μ a o Trans μ ( FObj T a ) ] ≈ A [ Trans μ a o FMap T (Trans μ a) ] ]
|
|
|
67 unity1 : {a : Obj A} -> A [ A [ Trans μ a o Trans η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
|
|
|
68 unity2 : {a : Obj A} -> A [ A [ Trans μ a o (FMap T (Trans η a ))] ≈ Id {_} {_} {_} {A} (FObj T a) ]
|
|
0
|
69
|
|
7
|
70 record Monad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (T : Functor A A) (η : NTrans A A identityFunctor T) (μ : NTrans A A (T ○ T) T)
|
|
1
|
71 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
|
|
7
|
72 eta : NTrans A A identityFunctor T
|
|
6
|
73 eta = η
|
|
7
|
74 mu : NTrans A A (T ○ T) T
|
|
6
|
75 mu = μ
|
|
1
|
76 field
|
|
|
77 isMonad : IsMonad A T η μ
|
|
0
|
78
|
|
2
|
79 open Monad
|
|
|
80 Lemma3 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ}
|
|
|
81 { T : Functor A A }
|
|
7
|
82 { η : NTrans A A identityFunctor T }
|
|
|
83 { μ : NTrans A A (T ○ T) T }
|
|
2
|
84 { a : Obj A } ->
|
|
|
85 ( M : Monad A T η μ )
|
|
7
|
86 -> A [ A [ Trans μ a o Trans μ ( FObj T a ) ] ≈ A [ Trans μ a o FMap T (Trans μ a) ] ]
|
|
2
|
87 Lemma3 = \m -> IsMonad.assoc ( isMonad m )
|
|
|
88
|
|
|
89
|
|
|
90 Lemma4 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A } { f : Hom A a b}
|
|
|
91 -> A [ A [ Id {_} {_} {_} {A} b o f ] ≈ f ]
|
|
|
92 Lemma4 = \a -> IsCategory.identityL ( Category.isCategory a )
|
|
0
|
93
|
|
3
|
94 Lemma5 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ}
|
|
|
95 { T : Functor A A }
|
|
7
|
96 { η : NTrans A A identityFunctor T }
|
|
|
97 { μ : NTrans A A (T ○ T) T }
|
|
3
|
98 { a : Obj A } ->
|
|
|
99 ( M : Monad A T η μ )
|
|
7
|
100 -> A [ A [ Trans μ a o Trans η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
|
|
3
|
101 Lemma5 = \m -> IsMonad.unity1 ( isMonad m )
|
|
|
102
|
|
|
103 Lemma6 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ}
|
|
|
104 { T : Functor A A }
|
|
7
|
105 { η : NTrans A A identityFunctor T }
|
|
|
106 { μ : NTrans A A (T ○ T) T }
|
|
3
|
107 { a : Obj A } ->
|
|
|
108 ( M : Monad A T η μ )
|
|
7
|
109 -> A [ A [ Trans μ a o (FMap T (Trans η a )) ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
|
|
3
|
110 Lemma6 = \m -> IsMonad.unity2 ( isMonad m )
|
|
|
111
|
|
|
112 -- T = M x A
|
|
0
|
113 -- nat of η
|
|
|
114 -- g ○ f = μ(c) T(g) f
|
|
|
115 -- h ○ (g ○ f) = (h ○ g) ○ f
|
|
|
116 -- η(b) ○ f = f
|
|
|
117 -- f ○ η(a) = f
|
|
|
118
|
|
4
|
119 record Kleisli { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )
|
|
|
120 ( T : Functor A A )
|
|
7
|
121 ( η : NTrans A A identityFunctor T )
|
|
|
122 ( μ : NTrans A A (T ○ T) T )
|
|
4
|
123 ( M : Monad A T η μ ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
|
|
5
|
124 monad : Monad A T η μ
|
|
|
125 monad = M
|
|
4
|
126 join : { a b : Obj A } -> ( c : Obj A ) ->
|
|
|
127 ( Hom A b ( FObj T c )) -> ( Hom A a ( FObj T b)) -> Hom A a ( FObj T c )
|
|
7
|
128 join c g f = A [ Trans μ c o A [ FMap T g o f ] ]
|
|
|
129
|
|
10
|
130
|
|
17
|
131 -- open import Relation.Binary.Core renaming (Trans to Trans1 )
|
|
7
|
132
|
|
17
|
133 -- module ≈-Reasoning {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) where
|
|
7
|
134
|
|
17
|
135 -- -- The code in Relation.Binary.EqReasoning cannot handle
|
|
|
136 -- -- heterogeneous equalities, hence the code duplication here.
|
|
7
|
137
|
|
17
|
138 -- refl-hom : {a b : Obj A }
|
|
|
139 -- { x y z : Hom A a b } →
|
|
|
140 -- A [ x ≈ x ]
|
|
|
141 -- refl-hom = IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory A ))
|
|
8
|
142
|
|
17
|
143 -- trans-hom : {a b : Obj A }
|
|
|
144 -- { x y z : Hom A a b } →
|
|
|
145 -- A [ x ≈ y ] → A [ y ≈ z ] → A [ x ≈ z ]
|
|
|
146 -- trans-hom b c = ( IsEquivalence.trans (IsCategory.isEquivalence ( Category.isCategory A ))) b c
|
|
5
|
147
|
|
17
|
148 -- infixr 2 _∎
|
|
|
149 -- infixr 2 _≈⟨_⟩_
|
|
|
150 -- infix 1 begin_
|
|
7
|
151
|
|
12
|
152
|
|
17
|
153 -- data _IsRelatedTo_ {a} {A1 : Set a} (x : A1) {b} {B : Set b} (y : B) :
|
|
|
154 -- Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
|
|
|
155 -- relTo : (x≈y : A [ x ≈ y ] ) → x IsRelatedTo y
|
|
|
156
|
|
|
157 -- begin_ : ∀ {a} {A1 : Set a} {x : A1} {b} {B : Set b} {y : B} →
|
|
|
158 -- x IsRelatedTo y → A [ x ≈ y ]
|
|
|
159 -- begin relTo x≈y = x≈y
|
|
|
160
|
|
|
161 -- _≈⟨_⟩_ : ∀ {a} {A1 : Set a} (x : A1) {b} {B : Set b} {y : B}
|
|
|
162 -- {c} {C : Set c} {z : C} →
|
|
|
163 -- A [ x ≈ y ] → y IsRelatedTo z → x IsRelatedTo z
|
|
|
164 -- _ ≈⟨ x≈y ⟩ relTo y≈z = relTo (trans-hom x≈y y≈z)
|
|
|
165
|
|
|
166 -- _∎ : ∀ {a} {A1 : Set a} (x : A1) → x IsRelatedTo x
|
|
|
167 -- _∎ _ = relTo refl-hom
|
|
7
|
168
|
|
17
|
169 -- -- hoge : {!!} -- {a b : Obj A } -> Rel ( Hom A a b ) (suc ℓ )
|
|
|
170 -- -- hoge = IsCategory.identityL (Category.isCategory A)
|
|
|
171
|
|
|
172 -- lemma11 : ? -- {a c : Obj A} { x : Hom A a c } {y : Hom A a c } -> x IsRelatedTo y
|
|
|
173 -- lemma11 = relTo ( IsCategory.identityL (Category.isCategory A) )
|
|
|
174
|
|
|
175 open import Relation.Binary.PropositionalEquality
|
|
|
176 open ≡-Reasoning
|
|
|
177
|
|
|
178 lemma60 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) -> ∀{n} -> ( Set n ) IsRelatedTo ( Set n )
|
|
|
179 lemma60 c = relTo refl
|
|
|
180
|
|
|
181 lemma12 : {c₁ c₂ ℓ : Level} (L : Category c₁ c₂ ℓ) { a b c : Obj L } ->
|
|
|
182 ( x : Hom L c a ) -> ( y : Hom L b c ) -> L [ x o y ] ≡ L [ x o y ]
|
|
|
183 lemma12 L x y = begin L [ x o y ] ∎
|
|
7
|
184
|
|
17
|
185 lemma13 : {c₁ c₂ ℓ : Level} (L : Category c₁ c₂ ℓ) { a b : Obj L } ( c : Obj L ) ->
|
|
|
186 ( x : Hom L c a ) -> L [ x o Id L c ] ≡ L [ x o Id L c ]
|
|
|
187 lemma13 L c x = begin L [ x o Id L c ] ∎
|
|
|
188
|
|
|
189 lemma14 : {c₁ c₂ ℓ : Level} (L : Category c₁ c₂ ℓ) { a b : Obj L } ( c : Obj L ) ->
|
|
|
190 ( x : Hom L c a ) -> x ≡ L [ x o Id L c ]
|
|
|
191 lemma14 L a x = {!!}
|
|
|
192
|
|
|
193 lemma15 : {c₁ c₂ ℓ : Level} (L : Category c₁ c₂ ℓ) { a b : Obj L } ( c : Obj L ) ->
|
|
|
194 ( x y z : Hom L c a ) -> x ≡ y -> L [ y ≈ z ] -> x ≡ z
|
|
|
195 lemma15 L x y z = {!!}
|
|
|
196
|
|
|
197 eq-func : {c₁ c₂ ℓ : Level} (L : Category c₁ c₂ ℓ) ->
|
|
|
198 { a b : Obj L } -> ( x : Hom L a b ) -> { x y : Hom L a b } ->
|
|
|
199 L [ x ≈ y ] -> Hom L a b
|
|
|
200 eq-func c x eq = {!!}
|
|
8
|
201
|
|
17
|
202 -- ≅-to-≡ : ∀ {a} {A : Set a} {x y : A} → x ≅ y → x ≡ y
|
|
|
203 -- ≅-to-≡ refl = refl
|
|
14
|
204
|
|
17
|
205 data _==_ {n} {c₁ c₂ ℓ : Level} {L : Category c₁ c₂ ℓ} { a b : Obj L } :
|
|
|
206 Hom L a b -> Hom L a b -> Set (suc (c₁ ⊔ c₂ ⊔ ℓ)) where
|
|
|
207 reflection : { x : Hom L a b } -> x == x
|
|
|
208 identityR : {f : Hom L a b} → ( L [ f o Id L b ] ) == f
|
|
|
209 identityL : {f : Hom L a b} → ( L [ Id L a o f ] ) == f
|
|
|
210 o-resp-≈ : {c : Obj L} {f g : Hom L a c } {h i : Hom L c b } → f == g → h == i → ( L [ h o f ] ) == ( L [ i o g ] )
|
|
|
211 associative : {B C : Obj L } {f : Hom L C b } {g : Hom L B C } {h : Hom L a B }
|
|
|
212 → ( L [ f o L [ g o h ] ] ) == ( L [ L [ f o g ] o h ] )
|
|
14
|
213
|
|
17
|
214 cat-== : {c₁ c₂ ℓ : Level} (L : Category c₁ c₂ ℓ) { a b : Obj L } { x y : Hom L a b } -> ( x == y ) -> x ≡ y
|
|
|
215 cat-== c reflection = ?
|
|
14
|
216
|
|
17
|
217 cat-eq : {c₁ c₂ ℓ : Level} (L : Category c₁ c₂ ℓ) { a b : Obj L } { x y : Hom L a b } -> L [ x ≈ y ] -> x ≡ y
|
|
|
218 cat-eq c refl = refl
|
|
4
|
219
|
|
11
|
220
|
|
|
221 Lemma61 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ->
|
|
17
|
222 { a : Obj A } ( b : Obj A ) ->
|
|
|
223 ( f : Hom A a b )
|
|
|
224 -> A [ (Id {_} {_} {_} {A} b) o f ] ≡ f
|
|
|
225 Lemma61 c b g = -- IsCategory.identityL (Category.isCategory c)
|
|
|
226 begin
|
|
|
227 c [ Id c b o g ]
|
|
|
228 ≡⟨ cat-eq c ( IsCategory.identityL (Category.isCategory c)) ⟩
|
|
|
229 g
|
|
|
230 ∎
|
|
11
|
231
|
|
4
|
232 open Kleisli
|
|
7
|
233 Lemma7 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ->
|
|
3
|
234 { T : Functor A A }
|
|
7
|
235 { η : NTrans A A identityFunctor T }
|
|
|
236 { μ : NTrans A A (T ○ T) T }
|
|
5
|
237 { a b : Obj A }
|
|
|
238 { f : Hom A a ( FObj T b) }
|
|
|
239 { M : Monad A T η μ }
|
|
|
240 ( K : Kleisli A T η μ M)
|
|
7
|
241 -> A [ join K b (Trans η b) f ≈ f ]
|
|
11
|
242 Lemma7 c k =
|
|
|
243 -- { a b : Obj c}
|
|
|
244 -- { T : Functor c c }
|
|
|
245 -- { η : NTrans c c identityFunctor T }
|
|
|
246 -- { f : Hom c a ( FObj T b) }
|
|
|
247 {!!}
|
|
|
248
|
|
7
|
249
|
|
5
|
250 Lemma8 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ}
|
|
|
251 { T : Functor A A }
|
|
7
|
252 { η : NTrans A A identityFunctor T }
|
|
|
253 { μ : NTrans A A (T ○ T) T }
|
|
4
|
254 { a b : Obj A }
|
|
|
255 { f : Hom A a ( FObj T b) }
|
|
|
256 { M : Monad A T η μ }
|
|
|
257 ( K : Kleisli A T η μ M)
|
|
7
|
258 -> A [ join K b f (Trans η a) ≈ f ]
|
|
|
259 Lemma8 k = {!!}
|
|
5
|
260
|
|
|
261 Lemma9 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ}
|
|
|
262 { T : Functor A A }
|
|
7
|
263 { η : NTrans A A identityFunctor T }
|
|
|
264 { μ : NTrans A A (T ○ T) T }
|
|
5
|
265 { a b c d : Obj A }
|
|
|
266 { f : Hom A a ( FObj T b) }
|
|
|
267 { g : Hom A b ( FObj T c) }
|
|
|
268 { h : Hom A c ( FObj T d) }
|
|
|
269 { M : Monad A T η μ }
|
|
|
270 ( K : Kleisli A T η μ M)
|
|
|
271 -> A [ join K d h (join K c g f) ≈ join K d ( join K d h g) f ]
|
|
6
|
272 Lemma9 k = {!!}
|
|
5
|
273
|
|
4
|
274
|
|
3
|
275
|
|
|
276
|
|
|
277
|
|
|
278 -- Kleisli :
|
|
|
279 -- Kleisli = record { Hom =
|
|
|
280 -- ; Hom = _⟶_
|
|
|
281 -- ; Id = IdProd
|
|
|
282 -- ; _o_ = _∘_
|
|
|
283 -- ; _≈_ = _≈_
|
|
|
284 -- ; isCategory = record { isEquivalence = record { refl = λ {φ} → ≈-refl {φ = φ}
|
|
|
285 -- ; sym = λ {φ ψ} → ≈-symm {φ = φ} {ψ}
|
|
|
286 -- ; trans = λ {φ ψ σ} → ≈-trans {φ = φ} {ψ} {σ}
|
|
|
287 -- }
|
|
|
288 -- ; identityL = identityL
|
|
|
289 -- ; identityR = identityR
|
|
|
290 -- ; o-resp-≈ = o-resp-≈
|
|
|
291 -- ; associative = associative
|
|
|
292 -- }
|
|
|
293 -- }
|
