Mercurial > hg > Members > kono > Proof > category

changeset 551:97b98b81e990

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix ...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 06 Apr 2017 04:15:57 +0900
parents c0078b03201c
children 09b1f66f7d7c
files SetsCompleteness.agda
diffstat 1 files changed, 15 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Tue Apr 04 13:51:48 2017 +0900
+++ b/SetsCompleteness.agda	Thu Apr 06 04:15:57 2017 +0900
@@ -176,9 +176,16 @@
 
 open snat
 
+snmeq :  { 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 ) → 
+         { snmapsi   snmapti : SO i } →  snmapsi ≡  snmapti → SO i
+snmeq s t i {pi} {.pi} refl   = pi
+
 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   }
+    ( s t :  snat sobj smap )
+    ( eq1 : ( i : OC ) →  snmap s i ≡  snmap t i ) →  
+     (( i j :  OC  )  → (f : I ) → smap f (snmeq s t i (eq1 i) ) ≡ (snmeq s t j (eq1 j)  )) → snat sobj smap
+snat1 SO SM s t eq1 eqcomm = record { snmap = λ i → snmeq s t i (eq1 i);   sncommute = λ {i} {j} f → eqcomm i j f   }
 
 ≡cong2 : { c : Level } { A B C : Set  c } { a a' : A } { b b' : B } ( f : A → B → C ) 
     →  a  ≡  a'
@@ -192,12 +199,10 @@
      → ( ( 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 → snat1 SO SM x y ) 
-              ( extensionality Sets  ( λ  i  → eq1 i ) )
-              ( extensionality Sets  ( λ  snm  → 
+snat-cong {_} {I} {OC} SO SM {s} {t}  eq1  eq2 eq3 =  ≡cong ( λ x  → snat1 SO SM s t eq1 x  ) 
                  ( extensionality Sets  ( λ  i  →  
                  ( extensionality Sets  ( λ  j  →  
-                 ( extensionality Sets  ( λ  f  →   irr2 snm i j f ( eq2s i j f (eq1 i)  snm (eq2 i j f ) ) {!!} ))))))))
+                 ( extensionality Sets  ( λ  f  →   irr2 (λ i →  snmeq s t i (eq1 i) )i j f ( eq2s i j f (eq1 i)  (λ i →  snmeq s t i (eq1 i) ){!!} {!!} (eq2 i j f ) ) {!!} ))))))
    where
       eq2s1 : { i j : OC } { f : I }  →  {si : SO i} { sj : SO j } 
            ( snm : ( i : OC ) → SO i ) → ( si ≡  snm i ) → ( sj ≡  snm j ) → SM {i} {j} f  si ≡ sj →  SM f ( snm i) ≡ snm j
@@ -213,8 +218,10 @@
                   open  import  Relation.Binary.PropositionalEquality
                   open ≡-Reasoning
       eq2s : ( i j : OC ) ( f : I )  →   ( snmap s i ≡  snmap t i ) → 
-           ( snm : ( i : OC ) → SO i ) → SM {i} {j} f ( snmap s i )   ≡ snmap s j →  SM f ( snm i) ≡ snm j
-      eq2s i j f eq1 snm eq2 =  eq2s1 snm {!!} {!!} eq2
+           ( snm : ( i : OC ) → SO i ) 
+            → snmap s i  ≡ snm i → snmap s j  ≡ snm j 
+            → SM {i} {j} f ( snmap s i )   ≡ snmap s j →  SM f ( snm i) ≡ snm j
+      eq2s i j f eq1 snm eq2 eq3 eq4   =  eq2s1 snm eq2 eq3 eq4
       irr3 : { i j : OC } { f : I }  →  {snmapsi :  SO i  }  → {snmapsj :  SO j  } →
            ( es et : SM f ( snmapsi )  ≡ snmapsj  )  → es  ≡ et
       irr3 refl refl = refl