Mercurial > hg > Members > kono > Proof > category

comparison yoneda.agda @ 191:45191dc3f78a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
nat continue...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 30 Aug 2013 15:28:57 +0900
parents b82d7b054f28
children d7e4b7b441be
comparison
equal deleted inserted replaced
190:b82d7b054f28 191:45191dc3f78a
190 ≈⟨ idL ⟩ 190 ≈⟨ idL ⟩
191 g 191 g
192 ∎ 192 ∎
193 ) ) ) 193 ) ) )
194 distr1 : {a b c : Obj A} {f : Hom A a b} {g : Hom A b c} → SetsAop [ y-nat (A [ g o f ]) ≈ SetsAop [ y-nat g o y-nat f ] ] 194 distr1 : {a b c : Obj A} {f : Hom A a b} {g : Hom A b c} → SetsAop [ y-nat (A [ g o f ]) ≈ SetsAop [ y-nat g o y-nat f ] ]
195 distr1 {a} {b} {c} {f} {g} = let open ≈-Reasoning (A) in -- (λ x g₁ → (A [ (A [ g o f] o g₁ ]) ≡ (λ x x₁ → A [ g o A [ f o x₁ ] ] ) 195 distr1 {a} {b} {c} {f} {g} = let open ≈-Reasoning (A) in -- (λ x g₁ → (A [ (A [ g o f] o g₁ ]))) ≡ (λ x x₁ → A [ g o A [ f o x₁ ] ] )
196 extensionality1 ( λ x → extensionality ( 196 extensionality1 ( λ x → extensionality (
197 λ h → ≈-≡ ( begin 197 λ h → ≈-≡ ( begin
198 A [ A [ g o f ] o h ] 198 A [ A [ g o f ] o h ]
199 ≈↑⟨ assoc ⟩ 199 ≈↑⟨ assoc ⟩
200 A [ g o A [ f o h ] ] 200 A [ g o A [ f o h ] ]
205 ------ 205 ------
206 -- 206 --
207 -- F : A → Sets ∈ Obj SetsAop 207 -- F : A → Sets ∈ Obj SetsAop
208 -- 208 --
209 -- F(a) ⇔ Nat(h_a,F) 209 -- F(a) ⇔ Nat(h_a,F)
210 -- 210 -- x ∈ F(a) , (g : Hom A b a) → ( FMap F g ) x
211 ------ 211 ------
212 212
213 F2Natmap : {a : Obj A} → {F : Obj SetsAop} → (x : Obj (Category.op A)) → Hom Sets (FObj (CF {a}) x) (FObj F x) 213 F2Natmap : {a : Obj A} → {F : Obj SetsAop} → {x : FObj F a} → (b : Obj (Category.op A)) → Hom Sets (FObj (CF {a}) b) (FObj F b)
214 F2Natmap = {!!} 214 F2Natmap {a} {F} {x} b = λ ( g : Hom A b a ) → ( FMap F g ) x
215 215
216 F2Nat : {a : Obj A} → {F : Obj SetsAop} → FObj F a → Hom SetsAop (CF {a}) F 216 F2Nat : {a : Obj A} → {F : Obj SetsAop} → FObj F a → Hom SetsAop (CF {a}) F
217 F2Nat {a} {F} x = record { TMap = F2Natmap {a} {F} ; isNTrans = isNTrans1 {a} } where 217 F2Nat {a} {F} x = record { TMap = F2Natmap {a} {F} {x} ; isNTrans = isNTrans1 } where
218 isNTrans1 : {a : Obj A } → IsNTrans (Category.op A) (Sets {c₂}) (CF {a}) F (F2Natmap {a} {F}) 218 commute : {a₁ b : Obj (Category.op A)} {f : Hom (Category.op A) a₁ b} →
219 isNTrans1 {a} = record { commute = {!!} } 219 Sets [ Sets [ FMap F f o F2Natmap {a} {F} {x} a₁ ] ≈ Sets [ F2Natmap {a} {F} {x} b o FMap CF f ] ]
220 commute {a₁} {b} {f} = extensionality ( λ (g : Hom A a₁ a ) →　? )
221 isNTrans1 : IsNTrans (Category.op A) (Sets {c₂}) (CF {a}) F (F2Natmap {a} {F})
222 isNTrans1 = record { commute = λ {a₁ b f} → commute {a₁} {b} {f} }
220 223
221 224
222 Nat2F : {a : Obj A} → {F : Obj SetsAop} → Hom SetsAop (CF {a}) F → FObj F a 225 Nat2F : {a : Obj A} → {F : Obj SetsAop} → Hom SetsAop (CF {a}) F → FObj F a
223 Nat2F = {!!} 226 Nat2F = {!!}
224 227