Mercurial > hg > Members > kono > Proof > category

changeset 14:2b005ec775b4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
not yet worked
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 08 Jul 2013 17:55:04 +0900
parents 7fa1b11a097a
children 730a4a59a7bd
files nat.agda
diffstat 1 files changed, 26 insertions(+), 21 deletions(-) [+]
line wrap: on
line diff
--- a/nat.agda	Mon Jul 08 11:00:05 2013 +0900
+++ b/nat.agda	Mon Jul 08 17:55:04 2013 +0900
@@ -149,39 +149,44 @@
   infixr 2 _≈⟨_⟩_ 
   infix  1 begin_
 
-  data _IsRelatedTo_  {a b : Obj A } ( x y : Hom A a b ) :
-                     Set (suc (c₁ ⊔ c₂ ⊔ ℓ ))   where
-     relTo :  (x≈y :  Category._≈_ A x y ) → x IsRelatedTo y
 
-  lemma11 :  {a c : Obj A} { x y : Hom A a c}  -> x IsRelatedTo y
-  lemma11 =  relTo ( IsCategory.identityL (Category.isCategory A)  )
+  data _IsRelatedTo_ {a} {A1 : Set ℓ} (x : A1) {b} {B : Set ℓ} (y : B) :
+                     Set (suc (c₁ ⊔ c₂ ⊔ ℓ ))  where
+    relTo : (x≈y : A [ x ≈ y ] ) → x IsRelatedTo y
 
-  begin_ : {a b : Obj A } { x y : Hom A a b} →
+  begin_ : ∀ {a} {A1 : Set a} {x : A1} {b} {B : Set b} {y : 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 ] → y IsRelatedTo z → x IsRelatedTo z
-  _ ≈⟨ x≈y ⟩ relTo y≈z  = relTo ( trans-hom x≈y y≈z )
+  _≈⟨_⟩_ : ∀ {a} {A1 : Set a} (x : A1) {b} {B : Set b} {y : B}
+             {c} {C : Set c} {z : C} →
+           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) → x IsRelatedTo x
-  _ ∎  = relTo ( refl-hom )
+  _∎ : ∀ {a} {A1 : Set a} (x : A1) → x IsRelatedTo x
+  _∎ _ = relTo refl-hom
+
+--  hoge : {!!} -- {a b : Obj A } -> Rel ( Hom A a b ) (suc  ℓ )
+--  hoge = IsCategory.identityL (Category.isCategory A) 
+
+--  lemma11 :  {a c : Obj A} { x : Hom A a c } {y : Hom A a c }  -> x IsRelatedTo y
+--  lemma11 =  relTo ( IsCategory.identityL (Category.isCategory A)  )
+
 
 
 Lemma61 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ->
                  { a b : Obj A } 
                  { f : Hom A a b }
                       -> A  [ A [ (Id {_} {_} {_} {A} b) o f ]  ≈ f ]
-Lemma61 c = -- IsCategory.identityL (Category.isCategory c) 
-     { a b : Obj c } 
-     { g : Hom c a b }
-     -> let open ≈-Reasoning c in
-     begin  
-          c [ (Id {_} {_} {_} {c} b) o g ]
-     ≈⟨ IsCategory.identityL (Category.isCategory c) ⟩
-          g
-     ∎
+Lemma61 c = IsCategory.identityL (Category.isCategory c) 
+--      { a b : Obj c } 
+--      { g : Hom c a b }
+--      -> let open ≈-Reasoning c in
+--      begin  
+--           c [ (Id {_} {_} {_} {c} b) o g ]
+--      ≈⟨ IsCategory.identityL (Category.isCategory c) ⟩
+--           g
+--      ∎
 
 open Kleisli
 Lemma7 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ->