Mercurial > hg > Members > kono > Proof > category

changeset 547:c0078b03201c

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 13:51:48 +0900
parents 73a5606fa362
children 03b851adc4fb 97b98b81e990
files SetsCompleteness.agda
diffstat 1 files changed, 21 insertions(+), 24 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Tue Apr 04 11:24:47 2017 +0900
+++ b/SetsCompleteness.agda	Tue Apr 04 13:51:48 2017 +0900
@@ -186,21 +186,6 @@
     →  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 )
@@ -212,18 +197,30 @@
               ( extensionality Sets  ( λ  snm  → 
                  ( extensionality Sets  ( λ  i  →  
                  ( extensionality Sets  ( λ  j  →  
-                 ( extensionality Sets  ( λ  f  →   irr2 snm i j f ? {!!} ))))))))
+                 ( extensionality Sets  ( λ  f  →   irr2 snm i j f ( eq2s i j f (eq1 i)  snm (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
+      eq2s1 {i} {j} {f} {si} {sj}  snm eq1 eq2 eq3 =  begin
+                 SM f ( snm i)  
+             ≡⟨ ≡cong (λ x → SM f x ) (sym eq1)  ⟩
+                 SM f si  
+             ≡⟨ eq3 ⟩
+                 sj  
+             ≡⟨ eq2 ⟩
+                snm j
+             ∎   where
+                  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
+      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 :  ( 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
+      irr2 snm i j f  es et = irr3 es et 
 
 
 open import HomReasoning