# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1491030181 -32400
# Node ID cb0d01f1eec9e94706b9e8af1a580b425ad34e87
# Parent  158aaded24b9836a49be34c9a516c1d4a703d834
fix

diff -r 158aaded24b9 -r cb0d01f1eec9 SetsCompleteness.agda
--- 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