Mercurial > hg > Members > kono > Proof > category

changeset 13:7fa1b11a097a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Reasoning on going...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 08 Jul 2013 11:00:05 +0900
parents 72397d77c932
children 2b005ec775b4
files nat.agda
diffstat 1 files changed, 12 insertions(+), 12 deletions(-) [+]
line wrap: on
line diff
--- a/nat.agda	Sun Jul 07 20:20:51 2013 +0900
+++ b/nat.agda	Mon Jul 08 11:00:05 2013 +0900
@@ -149,23 +149,23 @@
   infixr 2 _≈⟨_⟩_ 
   infix  1 begin_
 
-  data IsRelatedTo  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)  {a b : Obj A } ( x y : Hom A a b ) :
+  data _IsRelatedTo_  {a b : Obj A } ( x y : Hom A a b ) :
                      Set (suc (c₁ ⊔ c₂ ⊔ ℓ ))   where
-     relTo :  (x≈y :  Category._≈_ x  y  ) → IsRelatedTo A x y
+     relTo :  (x≈y :  Category._≈_ A x y ) → x IsRelatedTo 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)  )
+  lemma11 :  {a c : Obj A} { x y : Hom A a c}  -> x IsRelatedTo y
+  lemma11 =  relTo ( IsCategory.identityL (Category.isCategory A)  )
 
-  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 ]
+  begin_ : {a b : Obj A } { x y : Hom A a b} →
+           x IsRelatedTo y → A [ x ≈ y ]
   begin relTo x≈y = x≈y
 
   _≈⟨_⟩_ :   {a b : Obj A }
                 ( x : Hom A a b ) → { y z : Hom A a b } → 
-                A [ x ≈ y ] → IsRelatedTo A y z → IsRelatedTo A x z
-  a ≈⟨ x≈y ⟩ relTo y≈z  = relTo ( trans-hom x≈y y≈z )
+                A [ x ≈ y ] → y IsRelatedTo z → x IsRelatedTo z
+  _ ≈⟨ x≈y ⟩ relTo y≈z  = relTo ( trans-hom x≈y y≈z )
 
-  _∎ :   {a b : Obj A } (x : Hom A a b) → IsRelatedTo A x x
+  _∎ :   {a b : Obj A } (x : Hom A a b) → x IsRelatedTo x
   _ ∎  = relTo ( refl-hom )
 
 
@@ -175,12 +175,12 @@
                       -> A  [ A [ (Id {_} {_} {_} {A} b) o f ]  ≈ f ]
 Lemma61 c = -- IsCategory.identityL (Category.isCategory c) 
      { a b : Obj c } 
-     { f : Hom c a b }
+     { g : Hom c a b }
      -> let open ≈-Reasoning c in
      begin  
-          c [ (Id {_} {_} {_} {c} b) o f ]
+          c [ (Id {_} {_} {_} {c} b) o g ]
      ≈⟨ IsCategory.identityL (Category.isCategory c) ⟩
-          f
+          g
      ∎
 
 open Kleisli