Mercurial > hg > Members > kono > Proof > category

changeset 12:72397d77c932

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Reasoning complete!
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 07 Jul 2013 20:20:51 +0900
parents 2cbecadc56c1
children 7fa1b11a097a
files nat.agda
diffstat 1 files changed, 13 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/nat.agda	Sun Jul 07 19:20:37 2013 +0900
+++ b/nat.agda	Sun Jul 07 20:20:51 2013 +0900
@@ -151,7 +151,10 @@
 
   data IsRelatedTo  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)  {a b : Obj A } ( x y : Hom A a b ) :
                      Set (suc (c₁ ⊔ c₂ ⊔ ℓ ))   where
-    relTo :  (x≈y : A [ x ≈ y ] ) → IsRelatedTo A x y
+     relTo :  (x≈y :  Category._≈_ x  y  ) → IsRelatedTo A x y
+
+  lemma11 :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)  {a b : Obj A } ( x y : Hom A a b ) -> ?
+  lemma11 =  \c -> relTo ( IsCategory.identityL (Category.isCategory c)  )
 
   begin_ : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ}  {a b : Obj A } { x y : Hom A a b} →
            IsRelatedTo A x y → A [ x ≈ y ]
@@ -170,14 +173,15 @@
                  { a b : Obj A } 
                  { f : Hom A a b }
                       -> A  [ A [ (Id {_} {_} {_} {A} b) o f ]  ≈ f ]
-Lemma61 c = IsCategory.identityL (Category.isCategory c) 
-        
---      -> let open ≈-Reasoning c in
---      begin  
---           c [ (Id {_} {_} {_} {c} b) o f ]
---      ≈⟨ IsCategory.identityL (Category.isCategory c) ⟩
---           f
---      ∎
+Lemma61 c = -- IsCategory.identityL (Category.isCategory c) 
+     { a b : Obj c } 
+     { f : Hom c a b }
+     -> let open ≈-Reasoning c in
+     begin  
+          c [ (Id {_} {_} {_} {c} b) o f ]
+     ≈⟨ IsCategory.identityL (Category.isCategory c) ⟩
+          f
+     ∎
 
 open Kleisli
 Lemma7 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ->