Mercurial > hg > Members > kono > Proof > category

changeset 549:adef39d19884

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
snmeqeqt
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 06 Apr 2017 02:45:42 +0900
parents 03b851adc4fb
children c2ce1c6a3570
files SetsCompleteness.agda
diffstat 1 files changed, 73 insertions(+), 15 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Wed Apr 05 22:04:38 2017 +0900
+++ b/SetsCompleteness.agda	Thu Apr 06 02:45:42 2017 +0900
@@ -190,15 +190,6 @@
          → SM f (snmeq s t i (eqi)) ≡ snmeq s t j (eqj)
 snmc s t refl refl refl refl = refl
 
-snmc1 :  { c₂ : Level } { I OC :  Set  c₂ } { SO :  OC →  Set   c₂  } { SM : { i j :  OC  }  → (f : I )→  SO i → SO j }
-          ( s t :  snat SO SM  ) → { i j : OC } → { f :  I } →
-         { snmapsi   snmapti : SO i } →  (eqi : snmapsi ≡  snmapti ) → 
-         { snmapsj   snmaptj : SO j } →  (eqj : snmapsj ≡  snmaptj ) 
-         → ( SM f ( snmapsi )   ≡ snmapsj )
-         → ( SM f ( snmapti )   ≡ snmaptj ) → ( snm : (i : OC ) → SO i ) →
-            SM f (snm i) ≡ snm j
-snmc1 s t refl refl refl refl snm = {!!}
-
 snat1 :   { c₂ : Level }  { I OC :  Set  c₂ } ( SO :  OC →  Set  c₂ ) ( SM : { i j :  OC  }  → (f : I )→  SO i → SO j )
     →  ( s t :  snat SO SM   )
     → ( eq1 : ( i : OC ) → snmap s i ≡  snmap t i ) 
@@ -210,32 +201,64 @@
      sncommute = λ {i} {j} f → snmc s t (eq1 i) (eq1 j) (eq2 i j f ) (eq3 i j f )
    }
 
-≡cong2 : { c : Level } { A B C : Set  c } { a a' : A } { b b' : B } ( f : A → B → C ) 
+≡cong2 : { c c' : Level } { A B : Set  c } { C : Set  c' } { a a' : A } { b b' : B } ( f : A → B → C ) 
     →  a  ≡  a'
     →  b  ≡  b'
     →  f a b  ≡  f a' b'
 ≡cong2 _ refl refl = refl
 
+subst2 : { c c' : Level } { A B : Set  c } { C : Set  c' } { a a' : A } {  b b' : B } ( f : A → C ) ( g : B → C ) 
+    →  f a  ≡  g b
+    →  a  ≡  a'
+    →  b  ≡  b'
+    →  f a'  ≡  g  b'
+subst2 {_} {_} {A} {B} {C} { a} {.a}  {b} {.b} f g f=g refl refl = f=g
+
 snmeqeqs  : { c₂ : Level } { I OC :  Set  c₂ } ( SO :  OC →  Set   c₂  ) ( SM : { i j :  OC  }  → (f : I )→  SO i → SO j )
           ( s t :  snat SO SM  ) → ( i : OC ) →  ( eq1 : ( i : OC ) → snmap s i ≡  snmap t i ) →
-          snmeq s t i  (eq1 i )  ≡ snmap s i
+           snmap s i ≡ snmeq s t i  (eq1 i )  
 snmeqeqs SO SM s t i eq1  = lemma  (eq1 i) refl where
     lemma  :  { snmapsi   snmapti sm : SO i } → ( eq1 : snmapsi ≡  snmapti ) → ( snmapsi  ≡ sm ) →
-          snmeq s t i  eq1  ≡ sm
+          sm  ≡ snmeq s t i  eq1  
     lemma refl refl  = refl
     
 snmeqeqt  : { c₂ : Level } { I OC :  Set  c₂ } ( SO :  OC →  Set   c₂  ) ( SM : { i j :  OC  }  → (f : I )→  SO i → SO j )
           ( s t :  snat SO SM  ) → ( i : OC ) →  ( eq1 : ( i : OC ) → snmap s i ≡  snmap t i ) →
-          snmeq s t i  (eq1 i )  ≡ snmap t i
+           snmap t i ≡ snmeq s t i  (eq1 i )  
 snmeqeqt SO SM s t i eq1  = lemma  (eq1 i) refl where
     lemma  :  { snmapsi   snmapti sm : SO i } → ( eq1 : snmapsi ≡  snmapti ) → ( snmapti  ≡ sm ) →
-          snmeq s t i  eq1  ≡ sm
+          sm  ≡ snmeq s t i  eq1  
     lemma refl refl  = refl
 
+scomm2 : { c₂ : Level } { I OC :  Set  c₂ } ( SO :  OC →  Set   c₂  ) ( SM : { i j :  OC  }  → (f : I )→  SO i → SO j )
+          ( s t :  snat SO SM  ) → ( eq1 : ( i : OC ) → snmap s i ≡  snmap t i ) 
+         → ( i j : OC ) → ( f :  I )
+         → SM f ( snmap s i )   ≡ snmap s j 
+         → SM f (snmeq s t i (eq1 i)) ≡ snmeq s t j (eq1 j)
+scomm2 SO SM s t eq1 i j f eq2 =  lemma eq2 (snmeqeqs SO SM s t i eq1) (snmeqeqs SO SM s t j eq1)    where
+    lemma : { si sni : SO i} { sj snj : SO j  } →  ( SM f si  ≡ sj ) →  (si  ≡ sni )  →  (sj  ≡ snj ) → ( SM f sni  ≡ snj )
+    lemma eq1 eq2 eq3 = subst2 (λ x → SM f x) (λ y → y ) eq1 eq2 eq3
+
+tcomm2 : { c₂ : Level } { I OC :  Set  c₂ } ( SO :  OC →  Set   c₂  ) ( SM : { i j :  OC  }  → (f : I )→  SO i → SO j )
+          ( s t :  snat SO SM  ) → ( eq1 : ( i : OC ) → snmap s i ≡  snmap t i ) 
+         → ( i j : OC ) → ( f :  I )
+         → SM f ( snmap t i )   ≡ snmap t j 
+         → SM f (snmeq s t i (eq1 i)) ≡ snmeq s t j (eq1 j)
+tcomm2 SO SM s t eq1 i j f eq2 =  lemma eq2 (snmeqeqt SO SM s t i eq1) (snmeqeqt SO SM s t j eq1)    where
+    lemma : { si sni : SO i} { sj snj : SO j  } →  ( SM f si  ≡ sj ) →  (si  ≡ sni )  →  (sj  ≡ snj ) → ( SM f sni  ≡ snj )
+    lemma eq1 eq2 eq3 = subst2 (λ x → SM f x) (λ y → y ) eq1 eq2 eq3
+
+
+-- {!!} -- subst ( λ x  → SM f x ) ( λ x  →  x ) ? ? ? 
+
+-- irr : { c₂ : Level}  {d : Set c₂ }  { x y : d } ( eq eq' :  x  ≡ y ) → eq ≡ eq'
+-- irr refl refl = refl
+
 -- irr2 : { c₂ : Level}  {d : Set c₂ }  { x1 x2 y1 y2  : d } ( eqx :  x1  ≡ x2 )( eqy :  y1  ≡ y2 ) 
 --     ( eq1 :  x1  ≡ y1 ) ( eq2 :  x2  ≡ y2 ) →  eq1 ≡  eq2
 -- irr2 = ?
 
+
 snat-cong :  { c : Level }  { I OC :  Set  c }  ( SObj :  OC →  Set  c  ) ( SMap : { i j :  OC  }  → (f : I )→  SObj i → SObj j)  
          { s t :  snat SObj SMap   }
      → (( i : OC ) → snmap s i ≡  snmap t i )
@@ -243,7 +266,42 @@
      → ( ( i j : OC ) ( f : I ) →  SMap {i} {j} f ( snmap t i )   ≡ snmap t j )
      → s ≡ t
 snat-cong {_} {I} {OC} SO SM {s} {t}  eq1  eq2 eq3 = ≡cong2 ( λ x y →
-     record { snmap = λ i → x i  ; sncommute  = y x } )  (extensionality Sets  ( λ  i  →  eq1 i  ))  {!!}
+     record { snmap = λ i → x i  ; sncommute  = λ {i} {j} f → y x i j f  } )  (extensionality Sets  ( λ  i  →  eq1 i  ))  
+        ( extensionality Sets  ( λ  x  → 
+          ( extensionality Sets  ( λ  i  → 
+            ( extensionality Sets  ( λ  j  → 
+              ( extensionality Sets  ( λ  f  →  snat-irr x i j f 
+                   {!!}
+                   {!!}
+           )))))))) where
+   smi=pi : ( i j : OC )  (f : I ) 
+       →  { sm   : ( i : OC ) → SO i }
+       →  { smi   : SO i }
+       →  ( sm i ≡ smi )
+       →  ( eq1 : ( i : OC ) → snmap s i ≡  snmap t i )
+       →  smi  ≡  snmap s i
+   smi=pi i j f {sm}  refl eq1 = {!!}  where
+       lemma : { si ti : SO i }  →  (  si ≡  ti )  →  sm i  ≡  si 
+       lemma refl = {!!}
+   scomm1 : ( i j : OC )  (f : I ) 
+       →  ( sm   : ( i : OC ) → SO i )
+       →  { smfi smj  : SO j} 
+       →  ( sm j   ≡  sm j )
+       →   smfi  ≡ smj
+       →   SM f (sm i) ≡ sm j
+   scomm1 i j f = {!!}
+   scomm : {sm :  ( i : OC ) → SO i  }  ( i j : OC )  (f : I ) 
+       →  ( eq1 : ( i : OC ) → snmap s i ≡  snmap t i )  
+       →  ( eq2 : ( i j : OC ) ( f : I ) →  SM {i} {j} f ( snmap s i )   ≡ snmap s j )
+       →  SM f (sm i) ≡ sm j
+   scomm {sm} i j f eq1 eq2 = {!!} -- scomm1 i j f sm (eq1 j) ( ≡cong ( λ k → SM f ) ( eq1 i )) (eq2 i j f )
+   snat-irr1 :  (sm :  ( i : OC ) → SO i  ) ( i j : OC ) → ( f :  I ) →  { smfi smj : SO j }  → ( es et : smfi  ≡ smj ) → es ≡  et
+   snat-irr1 sm i j f refl refl = refl
+   snat-irr :  (sm :  ( i : OC ) → SO i  ) ( i j : OC ) → ( f :  I ) →  ( es et : SM f ( sm i )  ≡ sm j ) → es ≡  et
+   snat-irr sm i j f es et = snat-irr1 sm i j f es et 
+
+   snat-irr' :  (sm :  ( i : OC ) → SO i  ) ( i j : OC ) → ( f :  I ) →  { snmapsi   snmapti : SO i } →  snmapsi ≡  snmapti  →  snmapsi ≡ sm i  →  ( es et : SM f ( sm i )  ≡ sm j ) → es ≡  et
+   snat-irr' sm i j f {pi} {.pi} refl eq es et = snat-irr1 sm i j f es et 
 
 
 open import HomReasoning