Mercurial > hg > Members > kono > Proof > category

diff Comma.agda @ 492:c7b8017bcd4d

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 Mon, 13 Mar 2017 13:22:40 +0900
parents 08f9c8a59ff4
children bed3be9a4168
line wrap: on
line diff
--- a/Comma.agda	Mon Mar 13 10:41:07 2017 +0900
+++ b/Comma.agda	Mon Mar 13 13:22:40 2017 +0900
@@ -39,6 +39,7 @@
 _∙_ :  {a b c : CommaObj } → CommaHom b c → CommaHom a b → CommaHom a c
 _∙_ {a} {b} {c} f g = record { 
          arrow = A [ arrow f o arrow g ] ;
+         arrowg = B [ arrowg f o arrowg g ] ;
          comm  = comm1
      } where
         comm1 :  C [ C [ FMap G (B [ arrowg f o arrowg g ] ) o hom a ]  ≈ C [ hom c  o  FMap F (A [ arrow f o arrow g ]) ]  ]
@@ -61,7 +62,7 @@
            ∎ 
 
 CommaId : { a : CommaObj } → CommaHom a a
-CommaId {a} = record {  arrow = id1 A ( obj a ) ;  
+CommaId {a} = record {  arrow = id1 A ( obj a ) ;  arrowg = id1 B ( objb a ) ;  
       comm = comm2 } where
         comm2 :  C [ C [ FMap G (id1 B (objb a)) o hom a ]  ≈ C [ hom a  o  FMap F (id1 A (obj a)) ]  ]
         comm2 =  let open ≈-Reasoning C in begin