Mercurial > hg > Members > kono > Proof > category

comparison freyd2.agda @ 690:3d41a8edbf63

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix universal mapping done.
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 12 Nov 2017 01:29:47 +0900
parents fb9fc9652c04
children 917e51be9bbf
comparison
equal deleted inserted replaced
689:fb9fc9652c04 690:3d41a8edbf63
403 g 403 g
404 ∎ where 404 ∎ where
405 comm1 : B [ B [ FMap U g o hom (i a) ] ≈ B [ B [ FMap U g o tmap-η a ] o FMap (K B A a) g ] ] 405 comm1 : B [ B [ FMap U g o hom (i a) ] ≈ B [ B [ FMap U g o tmap-η a ] o FMap (K B A a) g ] ]
406 comm1 = let open ≈-Reasoning B in sym idR 406 comm1 = let open ≈-Reasoning B in sym idR
407 407
408 UM : UniversalMapping B A U (λ b → obj (i b)) (tmap-η) 408 UM : UniversalMapping B A U
409 UM = record { 409 UM = record {
410 F = λ b → obj (i b) ;
411 η = tmap-η ;
410 _* = λ f → arrow (solution f) ; 412 _* = λ f → arrow (solution f) ;
411 isUniversalMapping = record { 413 isUniversalMapping = record {
412 universalMapping = λ {a} {b} {f} → univ f ; 414 universalMapping = λ {a} {b} {f} → univ f ;
413 uniquness = unique 415 uniquness = unique
414 }} 416 }}