Mercurial > hg > Members > kono > Proof > category
annotate nat.agda @ 72:cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 26 Jul 2013 12:38:54 +0900 |
| parents | 709c1bde54dc |
| children | b75b5792bd81 |
| rev | line source |
|---|---|
|
72
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
1 |
| 0 | 2 |
| 3 -- Monad | |
| 4 -- Category A | |
| 5 -- A = Category | |
| 22 | 6 -- Functor T : A → A |
| 0 | 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 |
| 56 | 12 --open import Category.HomReasoning |
| 13 open import HomReasoning | |
| 14 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
|
15 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
|
16 |
|
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
17 module nat { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } |
|
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
18 { 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
|
19 { η : 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
|
20 { μ : NTrans A A (T ○ T) T } |
|
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
21 { M : Monad A T η μ } |
|
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
22 { K : Kleisli A T η μ M } where |
|
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
23 |
| 0 | 24 |
| 1 | 25 --T(g f) = T(g) T(f) |
| 26 | |
| 31 | 27 open Functor |
| 22 | 28 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 } |
| 29 → A [ ( FMap T (A [ g o f ] )) ≈ (A [ FMap T g o FMap T f ]) ] | |
| 30 Lemma1 = \t → IsFunctor.distr ( isFunctor t ) | |
| 0 | 31 |
| 32 | |
| 7 | 33 open NTrans |
| 1 | 34 Lemma2 : {c₁ c₂ l : Level} {A : Category c₁ c₂ l} {F G : Functor A A} |
| 22 | 35 → (μ : NTrans A A F G) → {a b : Obj A} { f : Hom A a b } |
| 30 | 36 → A [ A [ FMap G f o TMap μ a ] ≈ A [ TMap μ b o FMap F f ] ] |
| 22 | 37 Lemma2 = \n → IsNTrans.naturality ( isNTrans n ) |
| 0 | 38 |
| 22 | 39 -- η : 1_A → T |
| 40 -- μ : TT → T | |
| 0 | 41 -- μ(a)η(T(a)) = a |
| 42 -- μ(a)T(η(a)) = a | |
| 43 -- μ(a)(μ(T(a))) = μ(a)T(μ(a)) | |
| 44 | |
| 45 | |
| 2 | 46 open Monad |
| 47 Lemma3 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} | |
| 48 { T : Functor A A } | |
| 7 | 49 { η : NTrans A A identityFunctor T } |
| 50 { μ : NTrans A A (T ○ T) T } | |
| 22 | 51 { a : Obj A } → |
| 2 | 52 ( M : Monad A T η μ ) |
| 30 | 53 → A [ A [ TMap μ a o TMap μ ( FObj T a ) ] ≈ A [ TMap μ a o FMap T (TMap μ a) ] ] |
| 22 | 54 Lemma3 = \m → IsMonad.assoc ( isMonad m ) |
| 2 | 55 |
| 56 | |
| 57 Lemma4 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A } { f : Hom A a b} | |
| 22 | 58 → A [ A [ Id {_} {_} {_} {A} b o f ] ≈ f ] |
| 59 Lemma4 = \a → IsCategory.identityL ( Category.isCategory a ) | |
| 0 | 60 |
| 3 | 61 Lemma5 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} |
| 62 { T : Functor A A } | |
| 7 | 63 { η : NTrans A A identityFunctor T } |
| 64 { μ : NTrans A A (T ○ T) T } | |
| 22 | 65 { a : Obj A } → |
| 3 | 66 ( M : Monad A T η μ ) |
| 30 | 67 → A [ A [ TMap μ a o TMap η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ] |
| 22 | 68 Lemma5 = \m → IsMonad.unity1 ( isMonad m ) |
| 3 | 69 |
| 70 Lemma6 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} | |
| 71 { T : Functor A A } | |
| 7 | 72 { η : NTrans A A identityFunctor T } |
| 73 { μ : NTrans A A (T ○ T) T } | |
| 22 | 74 { a : Obj A } → |
| 3 | 75 ( M : Monad A T η μ ) |
| 30 | 76 → A [ A [ TMap μ a o (FMap T (TMap η a )) ] ≈ Id {_} {_} {_} {A} (FObj T a) ] |
| 22 | 77 Lemma6 = \m → IsMonad.unity2 ( isMonad m ) |
| 3 | 78 |
| 79 -- T = M x A | |
| 0 | 80 -- nat of η |
| 81 -- g ○ f = μ(c) T(g) f | |
| 82 -- η(b) ○ f = f | |
| 83 -- f ○ η(a) = f | |
| 22 | 84 -- h ○ (g ○ f) = (h ○ g) ○ f |
| 0 | 85 |
| 7 | 86 |
| 22 | 87 lemma12 : {c₁ c₂ ℓ : Level} (L : Category c₁ c₂ ℓ) { a b c : Obj L } → |
| 88 ( x : Hom L c a ) → ( y : Hom L b c ) → L [ L [ x o y ] ≈ L [ x o y ] ] | |
| 18 | 89 lemma12 L x y = |
| 90 let open ≈-Reasoning ( L ) in | |
| 91 begin L [ x o y ] ∎ | |
| 11 | 92 |
| 4 | 93 open Kleisli |
| 22 | 94 -- η(b) ○ f = f |
| 95 Lemma7 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) → | |
| 56 | 96 { T : Functor A A } |
| 21 | 97 ( η : NTrans A A identityFunctor T ) |
| 7 | 98 { μ : NTrans A A (T ○ T) T } |
| 21 | 99 { a : Obj A } ( b : Obj A ) |
| 100 ( f : Hom A a ( FObj T b) ) | |
| 22 | 101 ( m : Monad A T η μ ) |
| 56 | 102 { k : Kleisli A T η μ m} |
|
68
829e0698f87f
join implicit parameter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
66
diff
changeset
|
103 → A [ join k (TMap η b) f ≈ f ] |
| 56 | 104 Lemma7 c {T} η b f m {k} = |
| 21 | 105 let open ≈-Reasoning (c) |
| 106 μ = mu ( monad k ) | |
| 107 in | |
| 108 begin | |
|
68
829e0698f87f
join implicit parameter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
66
diff
changeset
|
109 join k (TMap η b) f |
| 21 | 110 ≈⟨ refl-hom ⟩ |
| 30 | 111 c [ TMap μ b o c [ FMap T ((TMap η b)) o f ] ] |
| 21 | 112 ≈⟨ IsCategory.associative (Category.isCategory c) ⟩ |
| 30 | 113 c [ c [ TMap μ b o FMap T ((TMap η b)) ] o f ] |
| 28 | 114 ≈⟨ car ( IsMonad.unity2 ( isMonad ( monad k )) ) ⟩ |
| 22 | 115 c [ id (FObj T b) o f ] |
| 21 | 116 ≈⟨ IsCategory.identityL (Category.isCategory c) ⟩ |
| 117 f | |
| 118 ∎ | |
| 7 | 119 |
| 22 | 120 -- f ○ η(a) = 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
|
121 Lemma8 : ( a : Obj A ) ( b : Obj A ) |
| 22 | 122 ( f : Hom A a ( FObj T b) ) |
|
72
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
123 → A [ join K f (TMap η a) ≈ f ] |
|
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
124 Lemma8 a b f = |
| 22 | 125 begin |
|
72
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
126 join K f (TMap η a) |
| 22 | 127 ≈⟨ 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
|
128 A [ TMap μ b o A [ FMap T f o (TMap η a) ] ] |
| 66 | 129 ≈⟨ 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
|
130 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
|
131 ≈⟨ 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
|
132 A [ A [ TMap μ b o (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
|
133 ≈⟨ car ( IsMonad.unity1 ( isMonad ( monad K )) ) ⟩ |
|
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
134 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
|
135 ≈⟨ IsCategory.identityL (Category.isCategory A) ⟩ |
| 22 | 136 f |
| 137 ∎ 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
|
138 open ≈-Reasoning (A) |
| 5 | 139 |
| 22 | 140 -- 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
|
141 Lemma9 : { a b c d : Obj A } |
| 23 | 142 ( f : Hom A a ( FObj T b) ) |
| 143 ( g : Hom A b ( FObj T c) ) | |
| 144 ( h : Hom A c ( FObj T d) ) | |
|
72
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
145 → A [ join K h (join K g f) ≈ join K ( join K h g) f ] |
|
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
146 Lemma9 {a} {b} {c} {d} f g h = |
| 24 | 147 begin |
|
72
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
148 join K h (join K g f) |
| 30 | 149 ≈⟨⟩ |
|
72
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
150 join K h ( ( TMap μ c o ( FMap T g o f ) ) ) |
| 28 | 151 ≈⟨ refl-hom ⟩ |
| 30 | 152 ( TMap μ d o ( FMap T h o ( TMap μ c o ( FMap T g o f ) ) ) ) |
| 28 | 153 ≈⟨ cdr ( cdr ( assoc )) ⟩ |
| 30 | 154 ( TMap μ d o ( FMap T h o ( ( TMap μ c o FMap T g ) o f ) ) ) |
| 28 | 155 ≈⟨ assoc ⟩ --- ( f o ( g o h ) ) = ( ( f o g ) o h ) |
| 30 | 156 ( ( TMap μ d o FMap T h ) o ( (TMap μ c o FMap T g ) o f ) ) |
| 25 | 157 ≈⟨ assoc ⟩ |
| 30 | 158 ( ( ( TMap μ d o FMap T h ) o (TMap μ c o FMap T g ) ) o f ) |
| 28 | 159 ≈⟨ car (sym assoc) ⟩ |
| 30 | 160 ( ( TMap μ d o ( FMap T h o ( TMap μ c o FMap T g ) ) ) o f ) |
| 28 | 161 ≈⟨ car ( cdr (assoc) ) ⟩ |
| 30 | 162 ( ( TMap μ d o ( ( FMap T h o TMap μ c ) o FMap T g ) ) o f ) |
| 28 | 163 ≈⟨ car assoc ⟩ |
| 30 | 164 ( ( ( TMap μ d o ( FMap T h o TMap μ c ) ) o FMap T g ) o f ) |
| 28 | 165 ≈⟨ car (car ( cdr ( begin |
| 30 | 166 ( FMap T h o TMap μ c ) |
| 66 | 167 ≈⟨ nat μ ⟩ |
| 30 | 168 ( TMap μ (FObj T d) o FMap T (FMap T h) ) |
| 25 | 169 ∎ |
| 170 ))) ⟩ | |
| 30 | 171 ( ( ( TMap μ d o ( TMap μ ( FObj T d) o FMap T ( FMap T h ) ) ) o FMap T g ) o f ) |
| 28 | 172 ≈⟨ car (sym assoc) ⟩ |
| 30 | 173 ( ( TMap μ d o ( ( TMap μ ( FObj T d) o FMap T ( FMap T h ) ) o FMap T g ) ) o f ) |
| 28 | 174 ≈⟨ car ( cdr (sym assoc) ) ⟩ |
| 30 | 175 ( ( TMap μ d o ( TMap μ ( FObj T d) o ( FMap T ( FMap T h ) o FMap T g ) ) ) o f ) |
| 28 | 176 ≈⟨ car ( cdr (cdr (sym (distr T )))) ⟩ |
| 30 | 177 ( ( TMap μ d o ( TMap μ ( FObj T d) o FMap T ( ( FMap T h o g ) ) ) ) o f ) |
| 28 | 178 ≈⟨ car assoc ⟩ |
| 30 | 179 ( ( ( TMap μ d o TMap μ ( FObj T d) ) o FMap T ( ( FMap T h o g ) ) ) o f ) |
| 28 | 180 ≈⟨ car ( car ( |
| 27 | 181 begin |
| 30 | 182 ( TMap μ d o TMap μ (FObj T d) ) |
|
72
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
183 ≈⟨ IsMonad.assoc ( isMonad M) ⟩ |
| 30 | 184 ( TMap μ d o FMap T (TMap μ d) ) |
| 27 | 185 ∎ |
| 186 )) ⟩ | |
| 30 | 187 ( ( ( TMap μ d o FMap T ( TMap μ d) ) o FMap T ( ( FMap T h o g ) ) ) o f ) |
| 28 | 188 ≈⟨ car (sym assoc) ⟩ |
| 30 | 189 ( ( TMap μ d o ( FMap T ( TMap μ d ) o FMap T ( ( FMap T h o g ) ) ) ) o f ) |
| 24 | 190 ≈⟨ sym assoc ⟩ |
| 30 | 191 ( TMap μ d o ( ( FMap T ( TMap μ d ) o FMap T ( ( FMap T h o g ) ) ) o f ) ) |
| 28 | 192 ≈⟨ cdr ( car ( sym ( distr T ))) ⟩ |
| 30 | 193 ( TMap μ d o ( FMap T ( ( ( TMap μ d ) o ( FMap T h o g ) ) ) o f ) ) |
| 23 | 194 ≈⟨ 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
|
195 join K ( ( TMap μ d o ( FMap T h o g ) ) ) f |
| 23 | 196 ≈⟨ 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
|
197 join K ( join K h g) f |
| 24 | 198 ∎ where open ≈-Reasoning (A) |
| 3 | 199 |
|
72
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
200 KHom1 : (a : Obj A) → (b : Obj A) -> Set (c₂ ⊔ c₁) |
| 70 | 201 KHom1 = {!!} |
| 202 | |
|
72
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
203 record KHom (a : Obj A) (b : Obj A) |
| 70 | 204 : Set (suc (c₂ ⊔ c₁)) where |
| 205 field | |
| 206 KMap : Hom A a ( FObj T b ) | |
|
69
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
68
diff
changeset
|
207 |
|
72
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
208 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
|
209 K-id {a = a} = record { KMap = TMap η a } |
| 56 | 210 |
|
69
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
68
diff
changeset
|
211 open import Relation.Binary.Core |
| 56 | 212 |
|
72
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
213 _⋍_ : |
|
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
214 { a : Obj A } { b : Obj A } (f g : KHom a b ) -> Set (suc ((c₂ ⊔ c₁) ⊔ ℓ)) |
|
71
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
215 _⋍_ = {!!} |
|
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
216 |
|
72
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
217 open KHom |
|
71
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
218 |
|
72
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
219 _*_ : { a b : Obj A } → { c : Obj A } → |
|
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
220 ( KHom b c) → ( KHom a b) → KHom a c |
|
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
221 _*_ {a} {b} {c} g f = record { KMap = join K {a} {b} {c} (KMap g) (KMap f) } |
| 70 | 222 |
|
72
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
223 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
|
224 isKleisliCategory = record { isEquivalence = isEquivalence |
|
71
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
225 ; identityL = KidL |
|
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
226 ; identityR = KidR |
|
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
227 ; o-resp-≈ = Ko-resp |
|
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
228 ; associative = Kassoc |
|
69
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
68
diff
changeset
|
229 } |
|
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
68
diff
changeset
|
230 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
|
231 isEquivalence : { a b : Obj A } -> |
|
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
232 IsEquivalence {_} {_} {KHom a b} _⋍_ |
|
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
233 isEquivalence {C} {D} = |
|
71
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
234 record { refl = λ {F} → ⋍-refl {F} |
|
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
235 ; sym = λ {F} {G} → ⋍-sym {F} {G} |
|
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
236 ; trans = λ {F} {G} {H} → ⋍-trans {F} {G} {H} |
|
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
237 } 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
|
238 ⋍-refl : {F : KHom C D} → F ⋍ F |
|
71
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
239 ⋍-refl = {!!} |
|
72
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
240 ⋍-sym : {F G : KHom C D} → F ⋍ G → G ⋍ F |
|
71
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
241 ⋍-sym = {!!} |
|
72
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
242 ⋍-trans : {F G H : KHom C D} → F ⋍ G → G ⋍ H → F ⋍ H |
|
71
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
243 ⋍-trans = {!!} |
|
72
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
244 KidL : {C D : Obj A} -> {f : KHom C D} → (K-id * f) ⋍ f |
|
69
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
68
diff
changeset
|
245 KidL = {!!} |
|
72
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
246 KidR : {C D : Obj A} -> {f : KHom C D} → (f * K-id) ⋍ f |
|
69
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
68
diff
changeset
|
247 KidR = {!!} |
|
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 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
|
249 f ⋍ g → h ⋍ i → (h * f) ⋍ (i * g) |
|
69
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
68
diff
changeset
|
250 Ko-resp = {!!} |
|
72
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
251 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
|
252 (f * (g * h)) ⋍ ((f * g) * h) |
|
69
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
68
diff
changeset
|
253 Kassoc = {!!} |
| 3 | 254 |
| 56 | 255 |