Mercurial > hg > Members > kono > Proof > category

comparison freyd2.agda @ 629:693020c766d2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 26 Jun 2017 17:41:02 +0900
parents b99660fa14e1
children d2fc6fb58e0e
comparison
equal deleted inserted replaced
628:b99660fa14e1 629:693020c766d2
245 open SmallFullSubcategory 245 open SmallFullSubcategory
246 open PreInitial 246 open PreInitial
247 247
248 ≡-cong = Relation.Binary.PropositionalEquality.cong 248 ≡-cong = Relation.Binary.PropositionalEquality.cong
249 249
250 ub : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (U : Functor A (Sets {c₂}) ) (b : Obj A) (x : FObj U b ) → Hom Sets (FObj (K Sets A *) b) (FObj U b)
251 ub A U b x OneObj = x
252 250
253 UisRepresentable : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 251 UisRepresentable : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
254 (U : Functor A (Sets {c₂}) ) 252 (U : Functor A (Sets {c₂}) )
255 (SFS : SmallFullSubcategory ( K (Sets {c₂}) A * ↓ U) ) 253 (SFS : SmallFullSubcategory ( K (Sets {c₂}) A * ↓ U) )
256 (pi : Obj ( K (Sets) A * ↓ U) ) 254 (PI : PreInitial ( K (Sets) A * ↓ U) (SFSF SFS))
257 (PI : PreInitial ( K (Sets) A * ↓ U) {pi} (SFSF SFS))
258 → Representable A U (obj (preinitialObj PI )) 255 → Representable A U (obj (preinitialObj PI ))
259 UisRepresentable A U SFS pi PI = record { 256 UisRepresentable A U SFS PI = record {
260 repr→ = record { TMap = tmap1 ; isNTrans = record { commute = comm1 } } 257 repr→ = record { TMap = tmap1 ; isNTrans = record { commute = comm1 } }
261 ; repr← = record { TMap = tmap2 ; isNTrans = record { commute = comm2 } } 258 ; repr← = record { TMap = tmap2 ; isNTrans = record { commute = comm2 } }
262 ; reprId→ = {!!} 259 ; reprId→ = {!!}
263 ; reprId← = {!!} 260 ; reprId← = {!!}
264 } where 261 } where
262 pi : Obj ( K (Sets) A * ↓ U)
263 pi = preinitialObj PI
264 ub : (b : Obj A) (x : FObj U b ) → Hom Sets (FObj (K Sets A *) b) (FObj U b)
265 ub b x OneObj = x
265 tmap1 : (b : Obj A) → Hom Sets (FObj U b) (FObj (Yoneda A (obj pi)) b) 266 tmap1 : (b : Obj A) → Hom Sets (FObj U b) (FObj (Yoneda A (obj pi)) b)
266 tmap1 b x = arrow ( SFSFMap← SFS ( preinitialArrow PI {FObj (SFSF SFS) (record { obj = b ; hom = ub A U b x}) } )) 267 tmap1 b x = arrow ( SFSFMap← SFS ( preinitialArrow PI {FObj (SFSF SFS) (record { obj = b ; hom = ub b x}) } ))
267 tmap2 : (b : Obj A) → Hom Sets (FObj (Yoneda A (obj (preinitialObj PI))) b) (FObj U b) 268 tmap2 : (b : Obj A) → Hom Sets (FObj (Yoneda A (obj (preinitialObj PI))) b) (FObj U b)
268 tmap2 b x = ( FMap U x ) ( hom ( preinitialObj PI ) OneObj ) 269 tmap2 b x = ( FMap U x ) ( hom ( preinitialObj PI ) OneObj )
270 comm11 : (a b : Obj A) (f : Hom A a b) (y : FObj U a ) →
271 ( Sets [ FMap (Yoneda A (obj (preinitialObj PI))) f o
272 ( λ x → arrow ( SFSFMap← SFS ( preinitialArrow PI {FObj (SFSF SFS) (record { obj = a ; hom = ub a x}) } ))) ] ) y
273 ≡ (Sets [ ( λ x → arrow ( SFSFMap← SFS ( preinitialArrow PI {FObj (SFSF SFS) (record { obj = b ; hom = ub b x}) } ))) o FMap U f ] ) y
274 comm11 a b f y = begin
275 ( Sets [ FMap (Yoneda A (obj (preinitialObj PI))) f o
276 ( λ x → arrow ( SFSFMap← SFS ( preinitialArrow PI {FObj (SFSF SFS) (record { obj = a ; hom = ub a x}) } ))) ] ) y
277 ≡⟨⟩
278 A [ f o arrow ( SFSFMap← SFS ( preinitialArrow PI {FObj (SFSF SFS) (record { obj = a ; hom = ub a y}) } )) ]
279 ≡⟨ {!!} ⟩
280 arrow ( SFSFMap← SFS ( preinitialArrow PI {FObj (SFSF SFS) (record { obj = b ; hom = ub b (FMap U f y) } ) } ) )
281 ≡⟨⟩
282 (Sets [ ( λ x → arrow ( SFSFMap← SFS ( preinitialArrow PI {FObj (SFSF SFS) (record { obj = b ; hom = ub b x}) } ))) o FMap U f ] ) y
283 ∎ where
284 open import Relation.Binary.PropositionalEquality
285 open ≡-Reasoning
269 comm1 : {a b : Obj A} {f : Hom A a b} → Sets [ Sets [ FMap (Yoneda A (obj (preinitialObj PI))) f o tmap1 a ] ≈ Sets [ tmap1 b o FMap U f ] ] 286 comm1 : {a b : Obj A} {f : Hom A a b} → Sets [ Sets [ FMap (Yoneda A (obj (preinitialObj PI))) f o tmap1 a ] ≈ Sets [ tmap1 b o FMap U f ] ]
270 comm1 {a} {b} {f} = let open ≈-Reasoning Sets in begin 287 comm1 {a} {b} {f} = let open ≈-Reasoning Sets in begin
271 FMap (Yoneda A (obj (preinitialObj PI))) f o tmap1 a 288 FMap (Yoneda A (obj (preinitialObj PI))) f o tmap1 a
272 ≈⟨ {!!} ⟩ 289 ≈⟨⟩
290 FMap (Yoneda A (obj (preinitialObj PI))) f o ( λ x → arrow ( SFSFMap← SFS ( preinitialArrow PI {FObj (SFSF SFS) (record { obj = a ; hom = ub a x}) } )))
291 ≈⟨ extensionality Sets ( λ y → comm11 a b f y ) ⟩
292 ( λ x → arrow ( SFSFMap← SFS ( preinitialArrow PI {FObj (SFSF SFS) (record { obj = b ; hom = ub b x}) } ))) o FMap U f
293 ≈⟨⟩
273 tmap1 b o FMap U f 294 tmap1 b o FMap U f
274 ∎ 295 ∎
275 comm21 : (a b : Obj A) (f : Hom A a b) ( y : Hom A (obj (preinitialObj PI)) a ) → 296 comm21 : (a b : Obj A) (f : Hom A a b) ( y : Hom A (obj (preinitialObj PI)) a ) →
276 (Sets [ FMap U f o (λ x → FMap U x (hom (preinitialObj PI) OneObj))] ) y ≡ 297 (Sets [ FMap U f o (λ x → FMap U x (hom (preinitialObj PI) OneObj))] ) y ≡
277 (Sets [ ( λ x → (FMap U x ) (hom (preinitialObj PI) OneObj)) o (λ x → A [ f o x ] ) ] ) y 298 (Sets [ ( λ x → (FMap U x ) (hom (preinitialObj PI) OneObj)) o (λ x → A [ f o x ] ) ] ) y