Mercurial > hg > Members > kono > Proof > category

comparison freyd2.agda @ 626:c5abbd39e6eb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
on going ...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 24 Jun 2017 08:34:36 +0900
parents d73fbed639a9
children efa1f2103a83
comparison
equal deleted inserted replaced
625:d73fbed639a9 626:c5abbd39e6eb
253 253
254 -- K{*}↓U has preinitial full subcategory then U is representable 254 -- K{*}↓U has preinitial full subcategory then U is representable
255 255
256 open SmallFullSubcategory 256 open SmallFullSubcategory
257 open PreInitial 257 open PreInitial
258 -- 258
259 -- UisRepresentable : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 259 ≡-cong = Relation.Binary.PropositionalEquality.cong
260 -- (U : Functor A (Sets {c₂}) ) 260
261 -- (a : Obj (Sets {c₂})) (ax : a) 261 isRepresentable : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
262 -- (SFS : SmallFullSubcategory {c₁} {c₂} {ℓ} ( K (Sets {c₂}) A a ↓ U) ) 262 (U : Functor A (Sets {c₂}) )
263 -- (PI : PreInitial {c₁} {c₂} {ℓ} ( K (Sets) A a ↓ U) (SFSF SFS )) 263 (SFS : SmallFullSubcategory {c₁} {c₂} {ℓ} ( K (Sets {c₂}) A * ↓ U) )
264 -- → Representable A U (obj (preinitialObj PI )) 264 (PI : PreInitial {c₁} {c₂} {ℓ} ( K (Sets) A * ↓ U) (SFSF SFS ))
265 -- UisRepresentable A U a ax SFS PI = record { 265 → Representable A U (obj (preinitialObj PI ))
266 -- repr→ = record { TMap = tmap1 ; isNTrans = record { commute = {!!} } } 266 isRepresentable A U SFS PI = record {
267 -- ; repr← = record { TMap = tmap2 ; isNTrans = record { commute = {!!} } } 267 repr→ = record { TMap = tmap1 ; isNTrans = record { commute = {!!} } }
268 -- ; reprId→ = λ {y} →　? 268 ; repr← = record { TMap = tmap2 ; isNTrans = record { commute = comm2 } }
269 -- ; reprId← = λ {y} →　? 269 ; reprId→ = λ {y} →　?
270 -- } where 270 ; reprId← = λ {y} →　?
271 -- tmap1 : (b : Obj A) → Hom Sets (FObj U b) (FObj (Yoneda A (obj (preinitialObj PI))) b) 271 } where
272 -- tmap1 b x = arrow ( SFSFMap← SFS ( preinitialArrow PI ) ) 272 tmap1 : (b : Obj A) → Hom Sets (FObj U b) (FObj (Yoneda A (obj (preinitialObj PI))) b)
273 -- tmap2 : (b : Obj A) → Hom Sets (FObj (Yoneda A (obj (preinitialObj PI))) b) (FObj U b) 273 tmap1 b x = arrow ( SFSFMap← SFS ( preinitialArrow PI ) )
274 -- tmap2 b x = ( FMap U x ) ( hom ( preinitialObj PI ) ax ) 274 tmap2 : (b : Obj A) → Hom Sets (FObj (Yoneda A (obj (preinitialObj PI))) b) (FObj U b)
275 tmap2 b x = ( FMap U x ) ( hom ( preinitialObj PI ) OneObj )
276 comm11 : (a b : Obj A) (f : Hom A a b) (y : FObj U a ) →
277 ( Sets [ FMap (Yoneda A (obj (preinitialObj PI))) f o ( λ x → arrow ( SFSFMap← SFS ( preinitialArrow PI ) ) )] ) y
278 ≡ ( Sets [( λ x → arrow ( SFSFMap← SFS ( preinitialArrow PI ) ) ) o FMap U f ] ) y
279 comm11 a b f y = begin
280 ( Sets [ FMap (Yoneda A (obj (preinitialObj PI))) f o ( λ x → arrow ( SFSFMap← SFS ( preinitialArrow PI ) ) )] ) y
281 ≡⟨⟩
282 ( FMap (Yoneda A (obj (preinitialObj PI))) f ) ( arrow ( SFSFMap← SFS ( preinitialArrow PI )))
283 ≡⟨⟩
284 A [ f o ( arrow ( SFSFMap← SFS ( preinitialArrow PI ))) ]
285 ≡⟨ {!!} ⟩
286 arrow ( SFSFMap← SFS ( preinitialArrow PI ))
287 ≡⟨⟩
288 ( Sets [( λ x → arrow ( SFSFMap← SFS ( preinitialArrow PI ) ) ) o FMap U f ] ) y
289 ∎ where
290 open import Relation.Binary.PropositionalEquality
291 open ≡-Reasoning
292 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 ] ]
293 comm1 {a} {b} {f} = let open ≈-Reasoning Sets in begin
294 FMap (Yoneda A (obj (preinitialObj PI))) f o tmap1 a
295 ≈⟨⟩
296 FMap (Yoneda A (obj (preinitialObj PI))) f o ( λ x → arrow ( SFSFMap← SFS ( preinitialArrow PI ) ) )
297 ≈⟨ extensionality Sets ( λ y → comm11 a b f y ) ⟩
298 ( λ x → arrow ( SFSFMap← SFS ( preinitialArrow PI ) ) ) o FMap U f
299 ≈⟨⟩
300 tmap1 b o FMap U f
301 ∎
302 comm21 : (a b : Obj A) (f : Hom A a b) ( y : Hom A (obj (preinitialObj PI)) a ) →
303 (Sets [ FMap U f o (λ x → FMap U x (hom (preinitialObj PI) OneObj))] ) y ≡
304 (Sets [ ( λ x → (FMap U x ) (hom (preinitialObj PI) OneObj)) o (λ x → A [ f o x ] ) ] ) y
305 comm21 a b f y = begin
306 FMap U f ( FMap U y (hom (preinitialObj PI) OneObj))
307 ≡⟨ ≡-cong ( λ k → k (hom (preinitialObj PI) OneObj)) ( sym ( IsFunctor.distr (isFunctor U ) ) ) ⟩
308 (FMap U (A [ f o y ] ) ) (hom (preinitialObj PI) OneObj)
309 ∎ where
310 open import Relation.Binary.PropositionalEquality
311 open ≡-Reasoning
312 comm2 : {a b : Obj A} {f : Hom A a b} → Sets [ Sets [ FMap U f o tmap2 a ] ≈
313 Sets [ tmap2 b o FMap (Yoneda A (obj (preinitialObj PI))) f ] ]
314 comm2 {a} {b} {f} = let open ≈-Reasoning Sets in begin
315 FMap U f o tmap2 a
316 ≈⟨⟩
317 FMap U f o ( λ x → ( FMap U x ) ( hom ( preinitialObj PI ) OneObj ) )
318 ≈⟨ extensionality Sets ( λ y → comm21 a b f y ) ⟩
319 ( λ x → ( FMap U x ) ( hom ( preinitialObj PI ) OneObj ) ) o ( λ x → A [ f o x ] )
320 ≈⟨⟩
321 ( λ x → ( FMap U x ) ( hom ( preinitialObj PI ) OneObj ) ) o FMap (Yoneda A (obj (preinitialObj PI))) f
322 ≈⟨⟩
323 tmap2 b o FMap (Yoneda A (obj (preinitialObj PI))) f
324 ∎