Mercurial > hg > Members > kono > Proof > category

changeset 545:cb0d01f1eec9

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 Sat, 01 Apr 2017 16:03:01 +0900
parents 158aaded24b9
children 73a5606fa362
files SetsCompleteness.agda
diffstat 1 files changed, 5 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Sat Apr 01 15:20:29 2017 +0900
+++ b/SetsCompleteness.agda	Sat Apr 01 16:03:01 2017 +0900
@@ -188,19 +188,16 @@
      → ( ( 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 → record { snmap = λ i → x i ; sncommute =  λ {i} {j} f → ?  } )  
               ( extensionality Sets  ( λ  i  → eq1 i ) )
               ( extensionality Sets  ( λ  i  → ( extensionality Sets  ( λ  j  → ( extensionality Sets  ( λ  f  → 
-                    irr1 i j f  ? ? ))))))
+                    irr2 (eq1 i) (eq1 j) {!!} {!!} ))))))
    where
-      irr1 : ( i j : OC ) ( f : I )  →  ( es et : SM f ( snmap s i )  ≡ snmap s j )  → es ≡ et 
-      irr1 i j f es et = {!!}
+      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
 
 
--- ( extensionality Sets ( λ i → eq1 i ) ) {!!}
---             (irr ( extensionality Sets ( λ i → ( extensionality Sets ( λ j → ( extensionality Sets ( λ f →  eq2 i j f ))))))
---                  ( extensionality Sets ( λ i → ( extensionality Sets ( λ j → ( extensionality Sets ( λ f →  eq3 i j f )))))))
-
 open import HomReasoning
 open NTrans