|
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
|
|
5
|
29 record IsNNAT {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (D : Category c₁ c₂ ℓ) (C : Category c₁′ c₂′ ℓ′)
|
|
0
|
30 ( F G : Functor D C )
|
|
5
|
31 (NAT : (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}
|
|
5
|
35 → C [ C [ ( FMap G f ) o ( NAT a ) ] ≈ C [ (NAT b ) o (FMap F f) ] ]
|
|
0
|
36 -- uniqness : {d : Obj D}
|
|
5
|
37 -- → C [ NAT d ≈ NAT d ]
|
|
0
|
38
|
|
|
39
|
|
5
|
40 record NNAT {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
|
|
5
|
43 NAT : (A : Obj domain) → Hom codomain (FObj F A) (FObj G A)
|
|
|
44 isNNAT : IsNNAT domain codomain F G NAT
|
|
0
|
45
|
|
5
|
46 open NNAT
|
|
1
|
47 Lemma2 : {c₁ c₂ l : Level} {A : Category c₁ c₂ l} {F G : Functor A A}
|
|
5
|
48 -> (μ : NNAT A A F G) -> {a b : Obj A} { f : Hom A a b }
|
|
|
49 -> A [ A [ FMap G f o NAT μ a ] ≈ A [ NAT μ b o FMap F f ] ]
|
|
|
50 Lemma2 = \n -> IsNNAT.naturality ( isNNAT 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 )
|
|
5
|
62 ( η : NNAT A A identityFunctor T )
|
|
|
63 ( μ : NNAT A A (T ○ T) T)
|
|
1
|
64 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
|
|
|
65 field
|
|
5
|
66 assoc : {a : Obj A} -> A [ A [ NAT μ a o NAT μ ( FObj T a ) ] ≈ A [ NAT μ a o FMap T (NAT μ a) ] ]
|
|
|
67 unity1 : {a : Obj A} -> A [ A [ NAT μ a o NAT η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
|
|
|
68 unity2 : {a : Obj A} -> A [ A [ NAT μ a o (FMap T (NAT η a ))] ≈ Id {_} {_} {_} {A} (FObj T a) ]
|
|
0
|
69
|
|
5
|
70 record Monad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (T : Functor A A) (η : NNAT A A identityFunctor T) (μ : NNAT A A (T ○ T) T)
|
|
1
|
71 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
|
|
|
72 field
|
|
|
73 isMonad : IsMonad A T η μ
|
|
0
|
74
|
|
2
|
75 open Monad
|
|
|
76 Lemma3 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ}
|
|
|
77 { T : Functor A A }
|
|
5
|
78 { η : NNAT A A identityFunctor T }
|
|
|
79 { μ : NNAT A A (T ○ T) T }
|
|
2
|
80 { a : Obj A } ->
|
|
|
81 ( M : Monad A T η μ )
|
|
5
|
82 -> A [ A [ NAT μ a o NAT μ ( FObj T a ) ] ≈ A [ NAT μ a o FMap T (NAT μ a) ] ]
|
|
2
|
83 Lemma3 = \m -> IsMonad.assoc ( isMonad m )
|
|
|
84
|
|
|
85
|
|
|
86 Lemma4 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A } { f : Hom A a b}
|
|
|
87 -> A [ A [ Id {_} {_} {_} {A} b o f ] ≈ f ]
|
|
|
88 Lemma4 = \a -> IsCategory.identityL ( Category.isCategory a )
|
|
0
|
89
|
|
3
|
90 Lemma5 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ}
|
|
|
91 { T : Functor A A }
|
|
5
|
92 { η : NNAT A A identityFunctor T }
|
|
|
93 { μ : NNAT A A (T ○ T) T }
|
|
3
|
94 { a : Obj A } ->
|
|
|
95 ( M : Monad A T η μ )
|
|
5
|
96 -> A [ A [ NAT μ a o NAT η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
|
|
3
|
97 Lemma5 = \m -> IsMonad.unity1 ( isMonad m )
|
|
|
98
|
|
|
99 Lemma6 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ}
|
|
|
100 { T : Functor A A }
|
|
5
|
101 { η : NNAT A A identityFunctor T }
|
|
|
102 { μ : NNAT A A (T ○ T) T }
|
|
3
|
103 { a : Obj A } ->
|
|
|
104 ( M : Monad A T η μ )
|
|
5
|
105 -> A [ A [ NAT μ a o (FMap T (NAT η a )) ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
|
|
3
|
106 Lemma6 = \m -> IsMonad.unity2 ( isMonad m )
|
|
|
107
|
|
|
108 -- T = M x A
|
|
0
|
109 -- nat of η
|
|
|
110 -- g ○ f = μ(c) T(g) f
|
|
|
111 -- h ○ (g ○ f) = (h ○ g) ○ f
|
|
|
112 -- η(b) ○ f = f
|
|
|
113 -- f ○ η(a) = f
|
|
|
114
|
|
4
|
115 record Kleisli { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )
|
|
|
116 ( T : Functor A A )
|
|
5
|
117 ( η : NNAT A A identityFunctor T )
|
|
|
118 ( μ : NNAT A A (T ○ T) T )
|
|
4
|
119 ( M : Monad A T η μ ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
|
|
5
|
120 monad : Monad A T η μ
|
|
|
121 monad = M
|
|
4
|
122 join : { a b : Obj A } -> ( c : Obj A ) ->
|
|
|
123 ( Hom A b ( FObj T c )) -> ( Hom A a ( FObj T b)) -> Hom A a ( FObj T c )
|
|
5
|
124 join c g f = A [ NAT μ c o A [ FMap T g o f ] ]
|
|
|
125
|
|
|
126 open import Relation.Binary
|
|
|
127 open import Relation.Binary.Core
|
|
4
|
128
|
|
|
129 open Kleisli
|
|
|
130 Lemma7 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ}
|
|
3
|
131 { T : Functor A A }
|
|
5
|
132 { η : NNAT A A identityFunctor T }
|
|
|
133 { μ : NNAT A A (T ○ T) T }
|
|
|
134 { a b : Obj A }
|
|
|
135 { f : Hom A a ( FObj T b) }
|
|
|
136 { M : Monad A T η μ }
|
|
|
137 ( K : Kleisli A T η μ M)
|
|
|
138 -> A [ join K b (NAT η b) f ≈ f ]
|
|
|
139 Lemma7 m = {!!}
|
|
|
140
|
|
|
141 Lemma8 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ}
|
|
|
142 { T : Functor A A }
|
|
|
143 { η : NNAT A A identityFunctor T }
|
|
|
144 { μ : NNAT A A (T ○ T) T }
|
|
4
|
145 { a b : Obj A }
|
|
|
146 { f : Hom A a ( FObj T b) }
|
|
|
147 { M : Monad A T η μ }
|
|
|
148 ( K : Kleisli A T η μ M)
|
|
5
|
149 -> A [ join K b f (NAT η a) ≈ f ]
|
|
|
150 Lemma8 m = {!!}
|
|
|
151
|
|
|
152 Lemma9 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ}
|
|
|
153 { T : Functor A A }
|
|
|
154 { η : NNAT A A identityFunctor T }
|
|
|
155 { μ : NNAT A A (T ○ T) T }
|
|
|
156 { a b c d : Obj A }
|
|
|
157 { f : Hom A a ( FObj T b) }
|
|
|
158 { g : Hom A b ( FObj T c) }
|
|
|
159 { h : Hom A c ( FObj T d) }
|
|
|
160 { M : Monad A T η μ }
|
|
|
161 ( K : Kleisli A T η μ M)
|
|
|
162 -> A [ join K d h (join K c g f) ≈ join K d ( join K d h g) f ]
|
|
|
163 Lemma9 m = {!!}
|
|
|
164
|
|
4
|
165
|
|
3
|
166
|
|
|
167
|
|
|
168
|
|
|
169 -- Kleisli :
|
|
|
170 -- Kleisli = record { Hom =
|
|
|
171 -- ; Hom = _⟶_
|
|
|
172 -- ; Id = IdProd
|
|
|
173 -- ; _o_ = _∘_
|
|
|
174 -- ; _≈_ = _≈_
|
|
|
175 -- ; isCategory = record { isEquivalence = record { refl = λ {φ} → ≈-refl {φ = φ}
|
|
|
176 -- ; sym = λ {φ ψ} → ≈-symm {φ = φ} {ψ}
|
|
|
177 -- ; trans = λ {φ ψ σ} → ≈-trans {φ = φ} {ψ} {σ}
|
|
|
178 -- }
|
|
|
179 -- ; identityL = identityL
|
|
|
180 -- ; identityR = identityR
|
|
|
181 -- ; o-resp-≈ = o-resp-≈
|
|
|
182 -- ; associative = associative
|
|
|
183 -- }
|
|
|
184 -- }
|
