Mercurial > hg > Members > kono > Proof > category

comparison freyd2.agda @ 651:1503af5d7440

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
id of Functor F
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 05 Jul 2017 07:53:07 +0900
parents 449025d1327f
children 236e916760e6
comparison
equal deleted inserted replaced
650:449025d1327f 651:1503af5d7440
397 identity = identity1 397 identity = identity1
398 ; distr = distr1 398 ; distr = distr1
399 ; ≈-cong = cong1 399 ; ≈-cong = cong1
400 } 400 }
401 } where 401 } where
402 id1comm : {a : Obj B} → B [ B [ FMap U (arrow (initial (In a) (ηf a a (id1 B a)))) o hom (i a) ]
403 ≈ B [ hom (i a) o FMap (K B A a) (arrow (initial (In a) (ηf a a (id1 B a)))) ] ]
404 id1comm {a} = let open ≈-Reasoning B in begin
405 FMap U (arrow (initial (In a) (ηf a a (id1 B a)))) o hom (i a)
406 ≈⟨ comm (initial (In a) (ηf a a (id1 B a))) ⟩
407 hom (ηf a a (id1 B a)) o FMap (K B A a) (arrow (initial (In a) (ηf a a (id1 B a))))
408 ≈⟨ idR ⟩
409 hom (ηf a a (id1 B a))
410 ≈⟨⟩
411 hom (i a) o id1 B a
412 ≈⟨ idR ⟩
413 hom (i a)
414 ≈↑⟨ idR ⟩
415 hom (i a) o FMap (K B A a) (arrow (initial (In a) (ηf a a (id1 B a))))
416 ∎
402 identity1 : {a : Obj B} → A [ arrow (initial (In a) (ηf a a (id1 B a))) ≈ id1 A (obj (i a)) ] 417 identity1 : {a : Obj B} → A [ arrow (initial (In a) (ηf a a (id1 B a))) ≈ id1 A (obj (i a)) ]
403 identity1 = {!!} 418 identity1 {a} = let open ≈-Reasoning A in begin
419 arrow (initial (In a) (ηf a a (id1 B a)))
420 ≈⟨ uniqueness (In a) (record { arrow = arrow (initial (In a) (ηf a a (id1 B a))); comm = id1comm }) ⟩
421 arrow (initial (In a) (i a))
422 ≈↑⟨ uniqueness (In a) (id1 ( K B A a ↓ U) (i a) ) ⟩
423 id1 A (obj (i a))
424 ∎
404 distr1 : {a b c : Obj B} {f : Hom B a b} {g : Hom B b c} → 425 distr1 : {a b c : Obj B} {f : Hom B a b} {g : Hom B b c} →
405 A [ arrow (initial (In a) (ηf a c (B [ g o f ]))) ≈ 426 A [ arrow (initial (In a) (ηf a c (B [ g o f ]))) ≈
406 A [ arrow (initial (In b) (ηf b c g)) o arrow (initial (In a) (ηf a b f)) ] ] 427 A [ arrow (initial (In b) (ηf b c g)) o arrow (initial (In a) (ηf a b f)) ] ]
407 distr1 = {!!} 428 distr1 = {!!}
408 cong1 : {a : Obj B} {b : Obj B} {f g : Hom B a b} → 429 cong1 : {a : Obj B} {b : Obj B} {f g : Hom B a b} →
420 ≈ A [ arrow (initial (In (FObj U b)) (record { obj = b ; hom = id1 B (FObj U b) })) o FMap (F ○ U) f ] ] 441 ≈ A [ arrow (initial (In (FObj U b)) (record { obj = b ; hom = id1 B (FObj U b) })) o FMap (F ○ U) f ] ]
421 comm1 = {!!} 442 comm1 = {!!}
422 443
423 nat-η : NTrans B B identityFunctor (U ○ F) 444 nat-η : NTrans B B identityFunctor (U ○ F)
424 nat-η = record { TMap = λ y → tmap-η y ; isNTrans = record { commute = comm1 } } where 445 nat-η = record { TMap = λ y → tmap-η y ; isNTrans = record { commute = comm1 } } where
425 comm1 : {a b : Obj B} {f : Hom B a b} 446 comm1 : {a b : Obj B} {f : Hom B a b} → B [ B [ FMap (U ○ F) f o tmap-η a ] ≈ B [ tmap-η b o f ] ]
426 → B [ B [ FMap (U ○ F) f o tmap-η a ]
427 ≈ B [ tmap-η b o f ] ]
428 comm1 {a} {b} {f} = let open ≈-Reasoning B in begin 447 comm1 {a} {b} {f} = let open ≈-Reasoning B in begin
429 FMap (U ○ F) f o tmap-η a 448 FMap (U ○ F) f o tmap-η a
430 ≈⟨⟩ 449 ≈⟨⟩
431 FMap U ( arrow ( initial (In a) (ηf a b f ))) o hom ( i a ) 450 FMap U ( arrow ( initial (In a) (ηf a b f ))) o hom ( i a )
432 ≈⟨ comm ( initial (In a) (ηf a b f)) ⟩ 451 ≈⟨ comm ( initial (In a) (ηf a b f)) ⟩