Mercurial > hg > Members > kono > Proof > category

comparison freyd2.agda @ 653:893ae9a95ee1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
solution
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 05 Jul 2017 09:55:31 +0900
parents 236e916760e6
children 2872af3b32cc
comparison
equal deleted inserted replaced
652:236e916760e6 653:893ae9a95ee1
386 sobj : {a : Obj B} {b : Obj A} → ( f : Hom B a (FObj U b) ) → CommaObj (K B A a) U 386 sobj : {a : Obj B} {b : Obj A} → ( f : Hom B a (FObj U b) ) → CommaObj (K B A a) U
387 sobj {a} {b} f = record {obj = b; hom = f } 387 sobj {a} {b} f = record {obj = b; hom = f }
388 solution : {a : Obj B} {b : Obj A} → ( f : Hom B a (FObj U b) ) → CommaHom (K B A a) U (i a) (sobj f) 388 solution : {a : Obj B} {b : Obj A} → ( f : Hom B a (FObj U b) ) → CommaHom (K B A a) U (i a) (sobj f)
389 solution {a} {b} f = initial (In a) (sobj f) 389 solution {a} {b} f = initial (In a) (sobj f)
390 390
391 univ : (a : Obj B) (b : Obj A) → (f : Hom B a (FObj U b)) 391 univ : {a : Obj B} {b : Obj A} → (f : Hom B a (FObj U b))
392 → B [ B [ FMap U (arrow (solution f)) o tmap-η a ] ≈ f ] 392 → B [ B [ FMap U (arrow (solution f)) o tmap-η a ] ≈ f ]
393 univ = {!!} 393 univ {a} {b} f = let open ≈-Reasoning B in begin
394 FMap U (arrow (solution f)) o tmap-η a
395 ≈⟨ comm (initial (In a) (sobj f)) ⟩
396 hom (sobj f) o FMap (K B A a) (arrow (initial (In a) (sobj f)))
397 ≈⟨ idR ⟩
398 f
399 ∎
394 400
395 ηf : (a b : Obj B) → ( f : Hom B a b ) → Obj ( K B A a ↓ U) 401 ηf : (a b : Obj B) → ( f : Hom B a b ) → Obj ( K B A a ↓ U)
396 ηf a b f = sobj ( B [ tmap-η b o f ] ) 402 ηf a b f = sobj ( B [ tmap-η b o f ] )
397 403
398 F : Functor B A 404 F : Functor B A