Mercurial > hg > Members > kono > Proof > category

diff HomReasoning.agda @ 606:92eb707498c7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix for new agda Set Completeness unfinnished
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 08 Jun 2017 19:26:12 +0900
parents a5034bdf6f38
children 984518c56e96
line wrap: on
line diff
--- a/HomReasoning.agda	Thu Jun 08 12:53:54 2017 +0900
+++ b/HomReasoning.agda	Thu Jun 08 19:26:12 2017 +0900
@@ -130,7 +130,7 @@
       →   A [ A [ FMap G f  o  TMap η a ]  ≈ A [ TMap η b  o  FMap F f ] ]
   nat1 η f =  IsNTrans.commute ( isNTrans η  )
 
-  infixr  2 _∎
+  infix  3 _∎
   infixr 2 _≈⟨_⟩_ _≈⟨⟩_ 
   infixr 2 _≈↑⟨_⟩_ 
   infix  1 begin_
@@ -168,9 +168,8 @@
                  ( f : Hom A a b )
                       →  A [ A [ (Id {_} {_} {_} {A} b) o f ]  ≈ f ]
 Lemma61 c b g = -- IsCategory.identityL (Category.isCategory c) 
-  let open ≈-Reasoning (c) in 
-     begin  
-          c [ Id {_} {_} {_} {c} b o g ]
+  let open ≈-Reasoning (c) in begin  
+          c [ ( Id {_} {_} {_} {c} b ) o g ]
      ≈⟨ IsCategory.identityL (Category.isCategory c) ⟩
           g
      ∎