Mercurial > hg > Members > kono > Proof > category

changeset 18:da1b8250e72a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
reasoning worked.
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 12 Jul 2013 11:39:06 +0900
parents 03d39cabebb7
children 93c0a2565d53
files list-nat.agda nat.agda
diffstat 2 files changed, 57 insertions(+), 93 deletions(-) [+]
line wrap: on
line diff
--- a/list-nat.agda	Thu Jul 11 19:37:35 2013 +0900
+++ b/list-nat.agda	Fri Jul 12 11:39:06 2013 +0900
@@ -24,12 +24,19 @@
 
 l3 = l1 ++ l2
 
+open  import  Relation.Binary.PropositionalEquality
+
 infixr 20  _==_
 
 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
+
+
+==-to-≡ :  ∀{n} {A : Set n}  {x y : List A} { a : A } -> x ==  y -> x ≡ y
+==-to-≡ = ?
+
 --      eq-nil  : [] == []
 
 list-id-l : { A : Set } -> { x : List A} ->  [] ++ x == x
@@ -50,7 +57,7 @@
 
 
 
-open  import  Relation.Binary.PropositionalEquality
+
 --open ≡-Reasoning
 
 cong1 : ∀{a} {A : Set a } {b} { B : Set b } ->
@@ -67,22 +74,26 @@
   infix  1 begin_
 
 
-  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
+  data _IsRelatedTo_ {a} {A1 : Set a} (x : List A) {b} {B : Set b} (y : List A) :
+                     Set n 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_ : ∀ {a} {A1 : Set a} {x : List A } {b} {B : Set b} {y : List A} →
+           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} →
+  _==⟨_⟩_ : ∀ {a} {A1 : Set a} (x : List A ) {b} {B : Set b} {y : List A}
+             {c} {C : Set c} {z : List A } →
             x == y  → y IsRelatedTo z → x IsRelatedTo z
-  _ ==⟨ x≈y ⟩ relTo y≈z = relTo (trans x≈y y≈z)
+  _ ==⟨ x≈y ⟩ relTo y≈z = relTo (trans-list (==-to-≡ x≈y) y≈z)
+
+  _∎ : ∀ {a} {A1 : Set a} (x : List A ) → x IsRelatedTo x
+  _∎ _ = relTo reflection
 
-  _∎ : ∀ {a} {A1 : Set a} (x : A1) → x IsRelatedTo x
-  _∎ _ = relTo refl
-
+lemma11 : {A : Set } ( x : List A ) -> x == x
+lemma11 x = {A : Set } {x : List A } -> let open ==-Reasoning A in
+     begin x ∎
+      
 ++-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)
--- a/nat.agda	Thu Jul 11 19:37:35 2013 +0900
+++ b/nat.agda	Fri Jul 12 11:39:06 2013 +0900
@@ -128,104 +128,57 @@
      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 : 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
-
---   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)
+  data _IsRelatedTo_ { a b : Obj A } ( x y : Hom A a b ) :
+                     Set (suc (c₁ ⊔ c₂ ⊔ ℓ ))  where
+    relTo : (x≈y : A [ x ≈ y ] ) → x IsRelatedTo y
 
---   _∎ : ∀ {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) 
+  begin_ : { a b : Obj A } { x y : Hom A a b } →
+           x IsRelatedTo y → A [ x ≈ y ]
+  begin relTo x≈y = x≈y
 
---   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)  )
+  _≈⟨_⟩_ : { 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)
 
-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
+  _∎ : { a b : Obj A } ( x : Hom A a b ) → x IsRelatedTo x
+  _∎ _ = relTo refl-hom
 
 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 ]  ∎
-
-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 = {!!}
-
--- ≅-to-≡ : ∀ {a} {A : Set a} {x y : A} → x ≅ y → x ≡ y
--- ≅-to-≡ refl = refl
-
-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 ] )
-
-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
-
+       ( x : Hom L c a ) -> ( y : Hom L b c ) -> L [ L [ x o y ] ≈ L [ x o y ] ]
+lemma12 L x y =  
+   let open ≈-Reasoning ( L )  in 
+      begin  L [ x o y ]  ∎
 
 Lemma61 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ->
                  { 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) 
+                      ->  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 ]
-     ≡⟨ cat-eq c ( IsCategory.identityL (Category.isCategory c)) ⟩
+          c [ Id {_} {_} {_} {c} b o g ]
+     ≈⟨ IsCategory.identityL (Category.isCategory c) ⟩
           g
      ∎