Mercurial > hg > Members > kono > Proof > category

changeset 546:73a5606fa362

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
on going
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 04 Apr 2017 11:24:47 +0900
parents cb0d01f1eec9
children c0078b03201c
files SetsCompleteness.agda
diffstat 1 files changed, 34 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Sat Apr 01 16:03:01 2017 +0900
+++ b/SetsCompleteness.agda	Tue Apr 04 11:24:47 2017 +0900
@@ -176,26 +176,54 @@
 
 open snat
 
+snat1 :   { c₂ : Level }  { I OC :  Set  c₂ } ( sobj :  OC →  Set  c₂ ) ( smap : { i j :  OC  }  → (f : I )→  sobj i → sobj j )
+    ( snm : ( i : OC ) → sobj i ) →  (( snm1 : ( i : OC ) → sobj i ) ( i j :  OC  )  → (f : I ) → smap f ( snm1 i )  ≡ snm1 j ) → snat sobj smap
+snat1 SO SM snm eq = record { snmap = λ i → snm i ;   sncommute = λ {i} {j} f → eq snm i j f   }
+
 ≡cong2 : { c : Level } { A B 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
 
+≡cong3 : { c : Level } { I OC A B C : Set  c } { a a' : OC → A } { b b' : I  → B } ( f : (OC → A ) → (I → B ) → C ) 
+    →  a  ≡  a'
+    →  b  ≡  b'
+    →  f  a  b  ≡  f a'  b'
+≡cong3 _ refl refl = refl
+
+
+snat-cong1 :  { 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   }
+     → ( snmap s  ≡  snmap t  )
+     → ( ( i j : OC ) ( f : I ) →  SMap {i} {j} f ( snmap s i )   ≡ snmap s j )
+     → ( ( i j : OC ) ( f : I ) →  SMap {i} {j} f ( snmap t i )   ≡ snmap t j )
+     → s ≡ t
+snat-cong1  SO SM eq eq1 eq2 = ≡cong3 ( λ x y → snat1 SO SM {!!} {!!} ) {!!} {!!}
+
 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 )
      → ( ( i j : OC ) ( f : I ) →  SMap {i} {j} f ( snmap s i )   ≡ snmap s j )
      → ( ( 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 =  λ {i} {j} f → ?  } )  
+snat-cong {_} {I} {OC} SO SM {s} {t}  eq1  eq2 eq3 =  ≡cong2 ( λ x y → snat1 SO SM x y ) 
               ( extensionality Sets  ( λ  i  → eq1 i ) )
-              ( extensionality Sets  ( λ  i  → ( extensionality Sets  ( λ  j  → ( extensionality Sets  ( λ  f  → 
-                    irr2 (eq1 i) (eq1 j) {!!} {!!} ))))))
+              ( extensionality Sets  ( λ  snm  → 
+                 ( extensionality Sets  ( λ  i  →  
+                 ( extensionality Sets  ( λ  j  →  
+                 ( extensionality Sets  ( λ  f  →   irr2 snm i j f ? {!!} ))))))))
    where
-      irr2 : { i j : OC } { f : I }  →  {snmapsi snmapti :  SO i  } {snmapsj snmaptj :  SO j  } → snmapsi ≡ snmapti → snmapsj ≡ snmaptj →
-           ( es et : SM f ( snmapsi )  ≡ snmapsj  )  → es ≡ et 
-      irr2 refl refl es et = irr es et
+      irr2 :  ( snm : ( i : OC ) → SO i ) ( i j : OC ) (f : I )  →  
+              ( es et : SM f (snm i )  ≡ snm j ) →  es  ≡ et 
+      irr2 _ _ _ _  es et = {!!}
+
+--      irr3 : { i j : OC } { f : I }  →  {snmapsi :  SO i  }  → {snmapsj :  SO j  } →
+--           ( es et : SM f ( snmapsi )  ≡ snmapsj  )  → es  ≡ et
+--      irr3 refl refl = refl
+--      irr2 : { i j : OC } { f : I }  →  {snmapsi snmapti :  SO i  } {snmapsj snmaptj :  SO j  } → snmapsi ≡ snmapti → snmapsj ≡ snmaptj →
+--           ( es : SM f ( snmapsi )  ≡ snmapsj  )    ( et :  SM f ( snmapti )  ≡ snmaptj  )   → {!!}
+--      irr2 refl refl es et = irr3 es et
 
 
 open import HomReasoning