Mercurial > hg > Members > kono > Proof > category

comparison freyd2.agda @ 638:a07b95e92933

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
creating nat
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 01 Jul 2017 10:21:34 +0900
parents 946ea019a2e7
children 4cf8f982dc5b
comparison
equal deleted inserted replaced
637:946ea019a2e7 638:a07b95e92933
243 -- A is complete and K{*}↓U has preinitial full subcategory then U is representable 243 -- A is complete and K{*}↓U has preinitial full subcategory then U is representable
244 244
245 open SmallFullSubcategory 245 open SmallFullSubcategory
246 open PreInitial 246 open PreInitial
247 247
248 -- if U preserve limit, K{*}↓U has initial object from freyd.agda
249
248 ≡-cong = Relation.Binary.PropositionalEquality.cong 250 ≡-cong = Relation.Binary.PropositionalEquality.cong
251
252
253 ub : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (U : Functor A (Sets {c₂}) )(b : Obj A) (x : FObj U b )
254 → Hom Sets (FObj (K Sets A *) b) (FObj U b)
255 ub A U b x OneObj = x
256 ob : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (U : Functor A (Sets {c₂}) )(b : Obj A) (x : FObj U b )
257 → Obj ( K Sets A * ↓ U)
258 ob A U b x = record { obj = b ; hom = ub A U b x}
259 fArrow : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (U : Functor A (Sets {c₂}) ) {a b : Obj A} (f : Hom A a b) (x : FObj U a )
260 → Hom ( K Sets A * ↓ U) ( ob A U a x ) (ob A U b (FMap U f x) )
261 fArrow A U {a} {b} f x = record { arrow = f ; comm = fArrowComm a b f x }
262 where
263 fArrowComm1 : (a b : Obj A) (f : Hom A a b) (x : FObj U a ) → (y : * ) → FMap U f ( ub A U a x y ) ≡ ub A U b (FMap U f x) y
264 fArrowComm1 a b f x OneObj = refl
265 fArrowComm : (a b : Obj A) (f : Hom A a b) (x : FObj U a ) →
266 Sets [ Sets [ FMap U f o hom (ob A U a x) ] ≈ Sets [ hom (ob A U b (FMap U f x)) o FMap (K Sets A *) f ] ]
267 fArrowComm a b f x = extensionality Sets ( λ y → begin
268 ( Sets [ FMap U f o hom (ob A U a x) ] ) y
269 ≡⟨⟩
270 FMap U f ( hom (ob A U a x) y )
271 ≡⟨⟩
272 FMap U f ( ub A U a x y )
273 ≡⟨ fArrowComm1 a b f x y ⟩
274 ub A U b (FMap U f x) y
275 ≡⟨⟩
276 hom (ob A U b (FMap U f x)) y
277 ∎ ) where
278 open import Relation.Binary.PropositionalEquality
279 open ≡-Reasoning
249 280
250 UpreserveLimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) ( comp : Complete A I ) 281 UpreserveLimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) ( comp : Complete A I )
251 (U : Functor A (Sets {c₂}) ) 282 (U : Functor A (Sets {c₂}) )
252 (SFS : SmallFullSubcategory ( K (Sets {c₂}) A * ↓ U) ) 283 (SFS : SmallFullSubcategory ( K (Sets {c₂}) A * ↓ U) )
253 (PI : PreInitial ( K (Sets) A * ↓ U) (SFSF SFS)) 284 (PI : PreInitial ( K (Sets) A * ↓ U) (SFSF SFS))
254 → LimitPreserve A I Sets U 285 → LimitPreserve A I Sets U
255 UpreserveLimit A I comp U SFS PI = record { 286 UpreserveLimit A I comp U SFS PI = record {
256 preserve = λ Γ lim → {!!} -- UpreserveLimit0 A I b Γ lim 287 preserve = λ Γ lim → limitInSets Γ lim
257 } 288 } where
289 limitInSets : (Γ : Functor I A) (lim : Limit A I Γ) →
290 IsLimit Sets I (U ○ Γ) (FObj U (a0 lim)) (LimitNat A I Sets Γ (a0 lim) (t0 lim) U)
291 limitInSets Γ lim = record {
292 limit = λ a t → ψ a t
293 ; t0f=t = λ {a t i} → t0f=t0 {a} {t} {i}
294 ; limit-uniqueness = λ {b} {t} {f} t0f=t → limit-uniqueness0 {b} {t} {f} t0f=t
295 } where
296 tacomm : (a : Obj Sets) ( t : NTrans I Sets (K Sets I a) (U ○ Γ) ) (x : a) {y : Obj I} {z : Obj I} {f : Hom I y z}
297 → A [ A [ FMap Γ f o arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) (ob A U (FObj Γ y) (TMap t y x))})) ] ≈
298 A [ arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) (ob A U (FObj Γ z) (TMap t z x))} ))
299 o FMap (K A I (obj (preinitialObj PI))) f ] ]
300 tacomm a t x {y} {z} {f} = let open ≈-Reasoning A in begin
301 FMap Γ f o arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) (ob A U (FObj Γ y) (TMap t y x))}))
302 ≈⟨⟩
303 arrow (fArrow A U (FMap Γ f) (TMap t y x ))
304 o arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) (ob A U (FObj Γ y) (TMap t y x))}))
305 ≈⟨ {!!} ⟩
306 arrow (SFSFMap← SFS (FMap (SFSF SFS) ( fArrow A U (FMap Γ f) (TMap t y x )) ))
307 o arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) (ob A U (FObj Γ y) (TMap t y x))}))
308 ≈⟨ {!!} ⟩
309 arrow (SFSFMap← SFS (( K (Sets) A * ↓ U) [ FMap (SFSF SFS) ( fArrow A U (FMap Γ f) (TMap t y x ))
310 o preinitialArrow PI {FObj (SFSF SFS) (ob A U (FObj Γ y) (TMap t y x))} ] ))
311 ≈⟨ {!!} ⟩
312 arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) (ob A U (FObj Γ z) (TMap t z x))} ))
313 ≈↑⟨ idR ⟩
314 arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) (ob A U (FObj Γ z) (TMap t z x))} ))
315 o FMap (K A I (obj (preinitialObj PI))) f
316 ∎
317 ta : (a : Obj Sets) ( t : NTrans I Sets (K Sets I a) (U ○ Γ) ) (x : a) → NTrans I A (K A I (obj (preinitialObj PI))) Γ
318 ta a t x = record { TMap = λ (a : Obj I ) →
319 arrow ( SFSFMap← SFS ( preinitialArrow PI {FObj (SFSF SFS) (ob A U (FObj Γ a) (TMap t a x))} ) )
320 ; isNTrans = record { commute = {!!} }} -- λ {a} {b} {f} → commute2 {a} {b} {f} }
321 ψ : (a : Obj Sets) → NTrans I Sets (K Sets I a) (U ○ Γ) → Hom Sets a (FObj U (a0 lim))
322 ψ a t x = FMap U (limit (isLimit lim) (obj (preinitialObj PI)) (ta a t x)) ( hom (preinitialObj PI) OneObj )
323 t0f=t0 : {a : Obj Sets} {t : NTrans I Sets (K Sets I a) (U ○ Γ)} {i : Obj I} →
324 Sets [ Sets [ TMap (LimitNat A I Sets Γ (a0 lim) (t0 lim) U) i o ψ a t ] ≈ TMap t i ]
325 t0f=t0 {a} {t} = {!!}
326 limit-uniqueness0 : {a : Obj Sets} {t : NTrans I Sets (K Sets I a) (U ○ Γ)} {f : Hom Sets a (FObj U (a0 lim))} →
327 ({i : Obj I} → Sets [ Sets [ TMap (LimitNat A I Sets Γ (a0 lim) (t0 lim) U) i o f ] ≈ TMap t i ]) → Sets [ ψ a t ≈ f ]
328 limit-uniqueness0 {a} {t} {f} = {!!}
258 329
259 -- if K{*}↓U has initial Obj, U is representable 330 -- if K{*}↓U has initial Obj, U is representable
260 331
261 UisRepresentable : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 332 UisRepresentable : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
262 (U : Functor A (Sets {c₂}) ) 333 (U : Functor A (Sets {c₂}) )
264 (In : HasInitialObject ( K (Sets) A * ↓ U) i ) 335 (In : HasInitialObject ( K (Sets) A * ↓ U) i )
265 → Representable A U (obj i) 336 → Representable A U (obj i)
266 UisRepresentable A U i In = record { 337 UisRepresentable A U i In = record {
267 repr→ = record { TMap = tmap1 ; isNTrans = record { commute = comm1 } } 338 repr→ = record { TMap = tmap1 ; isNTrans = record { commute = comm1 } }
268 ; repr← = record { TMap = tmap2 ; isNTrans = record { commute = comm2 } } 339 ; repr← = record { TMap = tmap2 ; isNTrans = record { commute = comm2 } }
269 ; reprId→ = {!!} 340 ; reprId→ = iso→
270 ; reprId← = {!!} 341 ; reprId← = iso←
271 } where 342 } where
272 ub : (b : Obj A) (x : FObj U b ) → Hom Sets (FObj (K Sets A *) b) (FObj U b)
273 ub b x OneObj = x
274 ob : (b : Obj A) (x : FObj U b ) → Obj ( K Sets A * ↓ U)
275 ob b x = record { obj = b ; hom = ub b x}
276 fArrowComm1 : (a b : Obj A) (f : Hom A a b) (x : FObj U a ) → (y : * ) → FMap U f ( ub a x y ) ≡ ub b (FMap U f x) y
277 fArrowComm1 a b f x OneObj = refl
278 fArrowComm : (a b : Obj A) (f : Hom A a b) (x : FObj U a ) →
279 Sets [ Sets [ FMap U f o hom (ob a x) ] ≈ Sets [ hom (ob b (FMap U f x)) o FMap (K Sets A *) f ] ]
280 fArrowComm a b f x = extensionality Sets ( λ y → begin
281 ( Sets [ FMap U f o hom (ob a x) ] ) y
282 ≡⟨⟩
283 FMap U f ( hom (ob a x) y )
284 ≡⟨⟩
285 FMap U f ( ub a x y )
286 ≡⟨ fArrowComm1 a b f x y ⟩
287 ub b (FMap U f x) y
288 ≡⟨⟩
289 hom (ob b (FMap U f x)) y
290 ∎ ) where
291 open import Relation.Binary.PropositionalEquality
292 open ≡-Reasoning
293 fArrow : {a b : Obj A} (f : Hom A a b) (x : FObj U a ) → Hom ( K Sets A * ↓ U) ( ob a x ) (ob b (FMap U f x) )
294 fArrow {a} {b} f x = record { arrow = f ; comm = fArrowComm a b f x }
295 comm11 : (a b : Obj A) (f : Hom A a b) (y : FObj U a ) → 343 comm11 : (a b : Obj A) (f : Hom A a b) (y : FObj U a ) →
296 ( Sets [ FMap (Yoneda A (obj i)) f o ( λ x → arrow (initial In (ob a x))) ] ) y 344 ( Sets [ FMap (Yoneda A (obj i)) f o ( λ x → arrow (initial In (ob A U a x))) ] ) y
297 ≡ (Sets [ ( λ x → arrow (initial In (ob b x))) o FMap U f ] ) y 345 ≡ (Sets [ ( λ x → arrow (initial In (ob A U b x))) o FMap U f ] ) y
298 comm11 a b f y = begin 346 comm11 a b f y = begin
299 ( Sets [ FMap (Yoneda A (obj i)) f o ( λ x → arrow (initial In (ob a x))) ] ) y 347 ( Sets [ FMap (Yoneda A (obj i)) f o ( λ x → arrow (initial In (ob A U a x))) ] ) y
300 ≡⟨⟩ 348 ≡⟨⟩
301 A [ f o arrow (initial In (ob a y)) ] 349 A [ f o arrow (initial In (ob A U a y)) ]
302 ≡⟨⟩ 350 ≡⟨⟩
303 A [ arrow ( fArrow f y ) o arrow (initial In (ob a y)) ] 351 A [ arrow ( fArrow A U f y ) o arrow (initial In (ob A U a y)) ]
304 ≡⟨ ≈-≡ A ( uniqueness In {ob b (FMap U f y) } (( K Sets A * ↓ U) [ fArrow f y o initial In (ob a y)] ) ) ⟩ 352 ≡⟨ ≈-≡ A ( uniqueness In {ob A U b (FMap U f y) } (( K Sets A * ↓ U) [ fArrow A U f y o initial In (ob A U a y)] ) ) ⟩
305 arrow (initial In (ob b (FMap U f y) )) 353 arrow (initial In (ob A U b (FMap U f y) ))
306 ≡⟨⟩ 354 ≡⟨⟩
307 (Sets [ ( λ x → arrow (initial In (ob b x))) o FMap U f ] ) y 355 (Sets [ ( λ x → arrow (initial In (ob A U b x))) o FMap U f ] ) y
308 ∎ where 356 ∎ where
309 open import Relation.Binary.PropositionalEquality 357 open import Relation.Binary.PropositionalEquality
310 open ≡-Reasoning 358 open ≡-Reasoning
311 tmap1 : (b : Obj A) → Hom Sets (FObj U b) (FObj (Yoneda A (obj i)) b) 359 tmap1 : (b : Obj A) → Hom Sets (FObj U b) (FObj (Yoneda A (obj i)) b)
312 tmap1 b x = arrow ( initial In (ob b x ) ) 360 tmap1 b x = arrow ( initial In (ob A U b x ) )
313 comm1 : {a b : Obj A} {f : Hom A a b} → Sets [ Sets [ FMap (Yoneda A (obj i)) f o tmap1 a ] ≈ Sets [ tmap1 b o FMap U f ] ] 361 comm1 : {a b : Obj A} {f : Hom A a b} → Sets [ Sets [ FMap (Yoneda A (obj i)) f o tmap1 a ] ≈ Sets [ tmap1 b o FMap U f ] ]
314 comm1 {a} {b} {f} = let open ≈-Reasoning Sets in begin 362 comm1 {a} {b} {f} = let open ≈-Reasoning Sets in begin
315 FMap (Yoneda A (obj i)) f o tmap1 a 363 FMap (Yoneda A (obj i)) f o tmap1 a
316 ≈⟨⟩ 364 ≈⟨⟩
317 FMap (Yoneda A (obj i)) f o ( λ x → arrow (initial In ( ob a x ))) 365 FMap (Yoneda A (obj i)) f o ( λ x → arrow (initial In ( ob A U a x )))
318 ≈⟨ extensionality Sets ( λ y → comm11 a b f y ) ⟩ 366 ≈⟨ extensionality Sets ( λ y → comm11 a b f y ) ⟩
319 ( λ x → arrow (initial In (ob b x))) o FMap U f 367 ( λ x → arrow (initial In (ob A U b x))) o FMap U f
320 ≈⟨⟩ 368 ≈⟨⟩
321 tmap1 b o FMap U f 369 tmap1 b o FMap U f
322 ∎ 370 ∎
323 comm21 : (a b : Obj A) (f : Hom A a b) ( y : Hom A (obj i) a ) → 371 comm21 : (a b : Obj A) (f : Hom A a b) ( y : Hom A (obj i) a ) →
324 (Sets [ FMap U f o (λ x → FMap U x (hom i OneObj))] ) y ≡ 372 (Sets [ FMap U f o (λ x → FMap U x (hom i OneObj))] ) y ≡
344 ( λ x → ( FMap U x ) ( hom i OneObj ) ) o FMap (Yoneda A (obj i)) f 392 ( λ x → ( FMap U x ) ( hom i OneObj ) ) o FMap (Yoneda A (obj i)) f
345 ≈⟨⟩ 393 ≈⟨⟩
346 tmap2 b o FMap (Yoneda A (obj i)) f 394 tmap2 b o FMap (Yoneda A (obj i)) f
347 ∎ 395 ∎
348 iso0 : ( x : Obj A) ( y : Hom A (obj i ) x ) ( z : * ) 396 iso0 : ( x : Obj A) ( y : Hom A (obj i ) x ) ( z : * )
349 → ( Sets [ FMap U y o hom i ] ) z ≡ ( Sets [ ub x (FMap U y (hom i OneObj)) o FMap (K Sets A *) y ] ) z 397 → ( Sets [ FMap U y o hom i ] ) z ≡ ( Sets [ ub A U x (FMap U y (hom i OneObj)) o FMap (K Sets A *) y ] ) z
350 iso0 x y OneObj = refl 398 iso0 x y OneObj = refl
351 iso→ : {x : Obj A} → Sets [ Sets [ tmap1 x o tmap2 x ] ≈ id1 Sets (FObj (Yoneda A (obj i)) x) ] 399 iso→ : {x : Obj A} → Sets [ Sets [ tmap1 x o tmap2 x ] ≈ id1 Sets (FObj (Yoneda A (obj i)) x) ]
352 iso→ {x} = let open ≈-Reasoning A in extensionality Sets ( λ ( y : Hom A (obj i ) x ) → ≈-≡ A ( begin 400 iso→ {x} = let open ≈-Reasoning A in extensionality Sets ( λ ( y : Hom A (obj i ) x ) → ≈-≡ A ( begin
353 ( Sets [ tmap1 x o tmap2 x ] ) y 401 ( Sets [ tmap1 x o tmap2 x ] ) y
354 ≈⟨⟩ 402 ≈⟨⟩
355 arrow ( initial In (ob x (( FMap U y ) ( hom i OneObj ) ))) 403 arrow ( initial In (ob A U x (( FMap U y ) ( hom i OneObj ) )))
356 ≈↑⟨ uniqueness In (record { arrow = y ; comm = extensionality Sets ( λ (z : * ) → iso0 x y z ) } ) ⟩ 404 ≈↑⟨ uniqueness In (record { arrow = y ; comm = extensionality Sets ( λ (z : * ) → iso0 x y z ) } ) ⟩
357 y 405 y
358 ∎ )) 406 ∎ ))
359 iso← : {x : Obj A} → Sets [ Sets [ tmap2 x o tmap1 x ] ≈ id1 Sets (FObj U x) ] 407 iso← : {x : Obj A} → Sets [ Sets [ tmap2 x o tmap1 x ] ≈ id1 Sets (FObj U x) ]
360 iso← {x} = extensionality Sets ( λ (y : FObj U x ) → ( begin 408 iso← {x} = extensionality Sets ( λ (y : FObj U x ) → ( begin
361 ( Sets [ tmap2 x o tmap1 x ] ) y 409 ( Sets [ tmap2 x o tmap1 x ] ) y
362 ≡⟨⟩ 410 ≡⟨⟩
363 ( FMap U ( arrow ( initial In (ob x y ) )) ) ( hom i OneObj ) 411 ( FMap U ( arrow ( initial In (ob A U x y ) )) ) ( hom i OneObj )
364 ≡⟨ ≡-cong (λ k → k OneObj) ( comm ( initial In (ob x y ) )) ⟩ 412 ≡⟨ ≡-cong (λ k → k OneObj) ( comm ( initial In (ob A U x y ) )) ⟩
365 hom (ob x y) OneObj 413 hom (ob A U x y) OneObj
366 ≡⟨⟩ 414 ≡⟨⟩
367 y 415 y
368 ∎ ) ) where 416 ∎ ) ) where
369 open import Relation.Binary.PropositionalEquality 417 open import Relation.Binary.PropositionalEquality
370 open ≡-Reasoning 418 open ≡-Reasoning