Mercurial > hg > Members > kono > Proof > category

changeset 17:03d39cabebb7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
not working yet
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 11 Jul 2013 19:37:35 +0900
parents 228147b118d6
children da1b8250e72a
files list-nat.agda nat.agda
diffstat 2 files changed, 130 insertions(+), 58 deletions(-) [+]
line wrap: on
line diff
--- a/list-nat.agda	Tue Jul 09 10:42:36 2013 +0900
+++ b/list-nat.agda	Thu Jul 11 19:37:35 2013 +0900
@@ -1,4 +1,6 @@
-module category where
+module list-nat where
+                                                                        
+open import Level
 
 
 postulate a : Set
@@ -24,9 +26,10 @@
 
 infixr 20  _==_
 
-data _==_ {A : Set} :  List A -> List A -> Set where
+data _==_ {n} {A : Set n} :  List A -> List A -> Set n where
       reflection  : {x : List A} -> x == x
       eq-cons : {x y : List A} { a : A } -> x ==  y -> ( a :: x ) == ( a :: y )
+      trans-list : {x y z : List A} { a : A } -> x ==  y -> y == z -> x == z
 --      eq-nil  : [] == []
 
 list-id-l : { A : Set } -> { x : List A} ->  [] ++ x == x
@@ -48,30 +51,58 @@
 
 
 open  import  Relation.Binary.PropositionalEquality
-open ≡-Reasoning
+--open ≡-Reasoning
 
-cong1 : {A : Set } { B : Set } ->
-   ( f : A -> B ) -> {x : A } -> {y : A} -> x ≡ y -> f x ≡ f y
-cong1 f refl = refl
+cong1 : ∀{a} {A : Set a } {b} { B : Set b } ->
+   ( f : List A -> List B ) -> {x : List A } -> {y : List A} -> x == y -> f x == f y
+cong1 f reflection = reflection
+cong1 f  ( eq-cons c ) = ?
+cong1 f  ( trans-list a b ) = ?
+
+module ==-Reasoning {n} (A : Set n) where
+
+
+  infixr  2 _∎
+  infixr 2 _==⟨_⟩_
+  infix  1 begin_
 
 
-++-assoc : {A : Set} ( xs ys zs : List A ) -> (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
-++-assoc [] ys zs = begin -- to prove ([] ++ ys) ++ zs ≡ [] ++ (ys ++ zs)
+  data _IsRelatedTo_ {a} {A1 : Set a} (x : A1) {b} {B : Set b} (y : A1) :
+                     Set (suc (a  ⊔ b)) where
+    relTo : (x≈y : x  ≡ y  ) → x IsRelatedTo y
+
+  begin_ : ∀ {a} {A1 : Set a} {x : A1} {b} {B : Set b} {y : A1} →
+           x IsRelatedTo y →  x  ≡ y 
+  begin relTo x≈y = x≈y
+
+  _==⟨_⟩_ : ∀ {a} {A1 : Set a} (x : A1) {b} {B : Set b} {y : A1}
+             {c} {C : Set c} {z : A1} →
+            x == y  → y IsRelatedTo z → x IsRelatedTo z
+  _ ==⟨ x≈y ⟩ relTo y≈z = relTo (trans x≈y y≈z)
+
+  _∎ : ∀ {a} {A1 : Set a} (x : A1) → x IsRelatedTo x
+  _∎ _ = relTo refl
+
+++-assoc : {L : Set} ( xs ys zs : List L ) -> (xs ++ ys) ++ zs  == xs ++ (ys ++ zs)
+++-assoc [] ys zs = {A : Set} -> let open ==-Reasoning A in
+  begin -- to prove ([] ++ ys) ++ zs  == [] ++ (ys ++ zs)
    ( [] ++ ys ) ++ zs
-  ≡⟨ refl ⟩
+  ==⟨ reflection ⟩
     ys ++ zs
-  ≡⟨ refl ⟩
+  ==⟨ reflection ⟩
     [] ++ ( ys ++ zs )
   ∎
-++-assoc (x :: xs) ys zs = begin -- to prove ((x :: xs) ++ ys) ++ zs ≡ (x :: xs) ++ (ys ++ zs)
+  
+++-assoc (x :: xs) ys zs = {A : Set} -> let open  ==-Reasoning A in
+  begin -- to prove ((x :: xs) ++ ys) ++ zs == (x :: xs) ++ (ys ++ zs)
     ((x :: xs) ++ ys) ++ zs
-  ≡⟨ refl ⟩
+  ==⟨ reflection ⟩
      (x :: (xs ++ ys)) ++ zs
-  ≡⟨ refl ⟩
+  ==⟨ reflection ⟩
     x :: ((xs ++ ys) ++ zs)
-  ≡⟨ cong1 (_::_ x) (++-assoc xs ys zs) ⟩ 
+  ==⟨ cong1 (_::_ x) (++-assoc xs ys zs) ⟩ 
     x :: (xs ++ (ys ++ zs))
-  ≡⟨ refl ⟩
+  ==⟨ reflection ⟩
     (x :: xs) ++ (ys ++ zs)
   ∎
 
--- a/nat.agda	Tue Jul 09 10:42:36 2013 +0900
+++ b/nat.agda	Thu Jul 11 19:37:35 2013 +0900
@@ -128,65 +128,106 @@
      join c g f = A [ Trans μ c  o A [ FMap T g  o f ] ]
 
 
-open import Relation.Binary.Core  renaming (Trans to Trans1 )
+-- open import Relation.Binary.Core  renaming (Trans to Trans1 )
 
-module ≈-Reasoning {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) where
+-- module ≈-Reasoning {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) where
 
-  -- The code in Relation.Binary.EqReasoning cannot handle                                                                              
-  -- heterogeneous equalities, hence the code duplication here.                                                                         
+--   -- The code in Relation.Binary.EqReasoning cannot handle                                                                              
+--   -- heterogeneous equalities, hence the code duplication here.                                                                         
 
-  refl-hom :   {a b : Obj A } 
-                { x y z : Hom A a b }  →
-        A [ x ≈ x ]
-  refl-hom =  IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory A ))
+--   refl-hom :   {a b : Obj A } 
+--                 { x y z : Hom A a b }  →
+--         A [ x ≈ x ]
+--   refl-hom =  IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory A ))
 
-  trans-hom :   {a b : Obj A } 
-                { x y z : Hom A a b }  →
-        A [ x ≈ y ] → A [ y ≈ z ] → A [ x ≈ z ]
-  trans-hom b c = ( IsEquivalence.trans (IsCategory.isEquivalence  ( Category.isCategory A ))) b c
+--   trans-hom :   {a b : Obj A } 
+--                 { x y z : Hom A a b }  →
+--         A [ x ≈ y ] → A [ y ≈ z ] → A [ x ≈ z ]
+--   trans-hom b c = ( IsEquivalence.trans (IsCategory.isEquivalence  ( Category.isCategory A ))) b c
 
-  infixr  2 _∎
-  infixr 2 _≈⟨_⟩_ 
-  infix  1 begin_
+--   infixr  2 _∎
+--   infixr 2 _≈⟨_⟩_ 
+--   infix  1 begin_
 
 
-  data _IsRelatedTo_ {a} {A1 : Set a} (x : A1) {b} {B : Set b} (y : B) :
-                     Set (suc (c₁ ⊔ c₂ ⊔ ℓ ))  where
-    relTo : (x≈y : A [ x ≈ y ] ) → x IsRelatedTo y
+--   data _IsRelatedTo_ {a} {A1 : Set a} (x : A1) {b} {B : Set b} (y : B) :
+--                      Set (suc (c₁ ⊔ c₂ ⊔ ℓ ))  where
+--     relTo : (x≈y : A [ x ≈ y ] ) → x IsRelatedTo y
+
+--   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} {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} {A1 : Set a} (x : A1) → x IsRelatedTo x
+--   _∎ _ = relTo refl-hom
 
-  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
+-- --  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)  )
+
+open  import  Relation.Binary.PropositionalEquality
+open ≡-Reasoning
+
+lemma60 :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ->  ∀{n} ->  ( Set n ) IsRelatedTo ( Set n )
+lemma60 c = relTo refl
+
+lemma12 :  {c₁ c₂ ℓ : Level} (L : Category c₁ c₂ ℓ) { a b c : Obj L } -> 
+       ( x : Hom L c a ) -> ( y : Hom L b c ) -> L [ x o y ] ≡ L [ x o y ]
+lemma12 L x y =  begin  L [ x o y ]  ∎
 
-  _≈⟨_⟩_ : ∀ {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)
+lemma13 :  {c₁ c₂ ℓ : Level} (L : Category c₁ c₂ ℓ) { a b : Obj L } ( c : Obj L ) -> 
+       ( x : Hom L c a ) -> L [ x o Id L c ] ≡ L [ x o Id L c ]
+lemma13 L c x  =  begin  L [ x o Id L c ]  ∎
+
+lemma14 : {c₁ c₂ ℓ : Level} (L : Category c₁ c₂ ℓ) { a b : Obj L } ( c : Obj L ) ->
+       ( x : Hom L c a ) -> x ≡ L [ x o Id L c ]
+lemma14 L a x = {!!}
+
+lemma15 : {c₁ c₂ ℓ : Level} (L : Category c₁ c₂ ℓ) { a b : Obj L } ( c : Obj L ) ->
+       ( x y z : Hom L c a ) -> x ≡ y -> L [ y  ≈  z ] -> x ≡ z
+lemma15 L x y z = {!!}
+
+eq-func : {c₁ c₂ ℓ : Level} (L : Category c₁ c₂ ℓ)  ->
+       { a b : Obj L } -> ( x : Hom L a b ) -> { x y : Hom L a b } ->
+       L [ x ≈ y ] -> Hom L a b
+eq-func c x eq = {!!}
 
-  _∎ : ∀ {a} {A1 : Set a} (x : A1) → x IsRelatedTo x
-  _∎ _ = relTo refl-hom
+-- ≅-to-≡ : ∀ {a} {A : Set a} {x y : A} → x ≅ y → x ≡ y
+-- ≅-to-≡ refl = refl
 
---  hoge : {!!} -- {a b : Obj A } -> Rel ( Hom A a b ) (suc  ℓ )
---  hoge = IsCategory.identityL (Category.isCategory A) 
+data _==_  {n} {c₁ c₂ ℓ : Level} {L : Category c₁ c₂ ℓ} { a b : Obj L } : 
+           Hom L a b -> Hom L a b -> Set  (suc (c₁ ⊔ c₂ ⊔ ℓ)) where
+     reflection : { x : Hom L a b } -> x == x
+     identityR :  {f : Hom L a b} → ( L [ f o Id L b ] ) == f
+     identityL :  {f : Hom L a b} → ( L [ Id L a o f ] ) == f
+     o-resp-≈ : {c : Obj L} {f g : Hom L a c } {h i : Hom L c b } → f == g → h == i → ( L [ h o f ] ) == ( L [ i o g ] )
+     associative : {B C : Obj L } {f : Hom L C b  }  {g : Hom L B C  } {h : Hom L a B }
+             → ( L [ f o L [ g o h ] ] ) == ( L [ L [ f o g ] o h ] )
 
---  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)  )
+cat-== : {c₁ c₂ ℓ : Level} (L : Category c₁ c₂ ℓ) { a b : Obj L } { x y : Hom L a b } -> ( x == y ) -> x ≡ y
+cat-== c reflection = ?
 
+cat-eq : {c₁ c₂ ℓ : Level} (L : Category c₁ c₂ ℓ) { a b : Obj L } { x y : Hom L a b } -> L [ x ≈ y ] -> x ≡ y
+cat-eq c refl = refl
 
 
 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
---      ∎
+                 { a : Obj A } ( b : Obj A ) ->
+                 ( f : Hom A a b )
+                      ->  A [ (Id {_} {_} {_} {A} b) o f ]  ≡ f
+Lemma61 c b g = --  IsCategory.identityL (Category.isCategory c) 
+     begin  
+          c [ Id c b o g ]
+     ≡⟨ cat-eq c ( IsCategory.identityL (Category.isCategory c)) ⟩
+          g
+     ∎
 
 open Kleisli
 Lemma7 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ->