Mercurial > hg > Members > kono > Proof > category

diff 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
line wrap: on
line diff
--- a/freyd2.agda	Sun Nov 12 00:53:32 2017 +0900
+++ b/freyd2.agda	Sun Nov 12 01:29:47 2017 +0900
@@ -405,8 +405,10 @@
          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 ] ]
          comm1 = let open ≈-Reasoning B in sym idR
 
-   UM : UniversalMapping B A U (λ b → obj (i b)) (tmap-η)
+   UM : UniversalMapping B A U 
    UM = record {
+         F = λ b → obj (i b) ;
+         η = tmap-η ;
          _* = λ f → arrow (solution f)  ;
          isUniversalMapping = record {
             universalMapping  = λ {a} {b} {f} → univ f ;