# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1491416684 -32400
# Node ID c2ce1c6a357028bbb1e62f8bb391b8e5fd19553e
# Parent  adef39d1988407722dc7c67a5e9370d1b657c930
close this

diff -r adef39d19884 -r c2ce1c6a3570 SetsCompleteness.agda
--- a/SetsCompleteness.agda	Thu Apr 06 02:45:42 2017 +0900
+++ b/SetsCompleteness.agda	Thu Apr 06 03:24:44 2017 +0900
@@ -234,8 +234,9 @@
           ( s t :  snat SO SM  ) → ( eq1 : ( i : OC ) → snmap s i ≡  snmap t i ) 
          → ( i j : OC ) → ( f :  I )
          → SM f ( snmap s i )   ≡ snmap s j 
-         → SM f (snmeq s t i (eq1 i)) ≡ snmeq s t j (eq1 j)
-scomm2 SO SM s t eq1 i j f eq2 =  lemma eq2 (snmeqeqs SO SM s t i eq1) (snmeqeqs SO SM s t j eq1)    where
+         → {x :  ( i : OC ) → SO i } → (x  ≡  λ i → snmeq s t i  (eq1 i )  )
+         → SM f (x i) ≡  x j
+scomm2 SO SM s t eq1 i j f eq2 refl =  lemma eq2 (snmeqeqs SO SM s t i eq1) (snmeqeqs SO SM s t j eq1)    where
     lemma : { si sni : SO i} { sj snj : SO j  } →  ( SM f si  ≡ sj ) →  (si  ≡ sni )  →  (sj  ≡ snj ) → ( SM f sni  ≡ snj )
     lemma eq1 eq2 eq3 = subst2 (λ x → SM f x) (λ y → y ) eq1 eq2 eq3
 
@@ -249,60 +250,29 @@
     lemma eq1 eq2 eq3 = subst2 (λ x → SM f x) (λ y → y ) eq1 eq2 eq3
 
 
--- {!!} -- subst ( λ x  → SM f x ) ( λ x  →  x ) ? ? ? 
-
--- irr : { c₂ : Level}  {d : Set c₂ }  { x y : d } ( eq eq' :  x  ≡ y ) → eq ≡ eq'
--- irr refl refl = refl
-
--- irr2 : { c₂ : Level}  {d : Set c₂ }  { x1 x2 y1 y2  : d } ( eqx :  x1  ≡ x2 )( eqy :  y1  ≡ y2 ) 
---     ( eq1 :  x1  ≡ y1 ) ( eq2 :  x2  ≡ y2 ) →  eq1 ≡  eq2
--- irr2 = ?
-
-
 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 → y x i j f  } )  (extensionality Sets  ( λ  i  →  eq1 i  ))  
-        ( extensionality Sets  ( λ  x  → 
-          ( extensionality Sets  ( λ  i  → 
-            ( extensionality Sets  ( λ  j  → 
-              ( extensionality Sets  ( λ  f  →  snat-irr x i j f 
-                   {!!}
-                   {!!}
-           )))))))) where
-   smi=pi : ( i j : OC )  (f : I ) 
-       →  { sm   : ( i : OC ) → SO i }
-       →  { smi   : SO i }
-       →  ( sm i ≡ smi )
-       →  ( eq1 : ( i : OC ) → snmap s i ≡  snmap t i )
-       →  smi  ≡  snmap s i
-   smi=pi i j f {sm}  refl eq1 = {!!}  where
-       lemma : { si ti : SO i }  →  (  si ≡  ti )  →  sm i  ≡  si 
-       lemma refl = {!!}
-   scomm1 : ( i j : OC )  (f : I ) 
-       →  ( sm   : ( i : OC ) → SO i )
-       →  { smfi smj  : SO j} 
-       →  ( sm j   ≡  sm j )
-       →   smfi  ≡ smj
-       →   SM f (sm i) ≡ sm j
-   scomm1 i j f = {!!}
-   scomm : {sm :  ( i : OC ) → SO i  }  ( i j : OC )  (f : I ) 
-       →  ( eq1 : ( i : OC ) → snmap s i ≡  snmap t i )  
-       →  ( eq2 : ( i j : OC ) ( f : I ) →  SM {i} {j} f ( snmap s i )   ≡ snmap s j )
-       →  SM f (sm i) ≡ sm j
-   scomm {sm} i j f eq1 eq2 = {!!} -- scomm1 i j f sm (eq1 j) ( ≡cong ( λ k → SM f ) ( eq1 i )) (eq2 i j f )
-   snat-irr1 :  (sm :  ( i : OC ) → SO i  ) ( i j : OC ) → ( f :  I ) →  { smfi smj : SO j }  → ( es et : smfi  ≡ smj ) → es ≡  et
-   snat-irr1 sm i j f refl refl = refl
-   snat-irr :  (sm :  ( i : OC ) → SO i  ) ( i j : OC ) → ( f :  I ) →  ( es et : SM f ( sm i )  ≡ sm j ) → es ≡  et
-   snat-irr sm i j f es et = snat-irr1 sm i j f es et 
-
-   snat-irr' :  (sm :  ( i : OC ) → SO i  ) ( i j : OC ) → ( f :  I ) →  { snmapsi   snmapti : SO i } →  snmapsi ≡  snmapti  →  snmapsi ≡ sm i  →  ( es et : SM f ( sm i )  ≡ sm j ) → es ≡  et
-   snat-irr' sm i j f {pi} {.pi} refl eq es et = snat-irr1 sm i j f es et 
-
+snat-cong {_} {I} {OC} SO SM {s} {t}  eq1  eq2 eq3 =  begin
+     record { snmap = λ i →  snmap s i ; sncommute  = λ {i} {j} f → sncommute s f  }
+ ≡⟨ 
+    ≡cong2 ( λ x y →
+      record { snmap = λ i → x i  ; sncommute  = λ {i} {j} f → y ? i j f } )  (  extensionality Sets  ( λ  i  →  snmeqeqs SO SM s t i eq1  ) )
+           ( extensionality Sets  ( λ  x  → 
+           ( extensionality Sets  ( λ  i  → 
+             ( extensionality Sets  ( λ  j  → 
+               ( extensionality Sets  ( λ  f  →  scomm2 SO SM s t eq1 i j f (eq2 i j f  ) x
+             ))))))))
+  ⟩
+     record { snmap = λ i → snmeq s t i  (eq1 i )  ; sncommute  = λ {i} {j} f →  snmc s t (eq1 i) (eq1 j) (eq2 i j f ) (eq3 i j f ) }
+ ≡⟨ {!!} ⟩
+     record { snmap = λ i →  snmap t i ; sncommute  = λ {i} {j} f → sncommute t f  }
+             ∎   where
+                  open  import  Relation.Binary.PropositionalEquality
+                  open ≡-Reasoning
 
 open import HomReasoning
 open NTrans