# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1496389849 -32400
# Node ID d3b669722d77c553db36c7218069a30e10250747
# Parent  2e3459a9a69fb9a0a482501ea577a85cd8fe880a
fix

diff -r 2e3459a9a69f -r d3b669722d77 SetsCompleteness.agda
--- a/SetsCompleteness.agda	Fri Jun 02 15:45:15 2017 +0900
+++ b/SetsCompleteness.agda	Fri Jun 02 16:50:49 2017 +0900
@@ -174,31 +174,6 @@
 
 open snat
 
-snmeq :  { c₂ : Level } { I OC :  Set  c₂ } { SO :  OC →  Set   c₂  } { SM : { i j :  OC  }  → (f : I  →  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
-
-snmc :  { c₂ : Level } { I OC :  Set  c₂ } { SO :  OC →  Set   c₂  } { SM : { i j :  OC  }  → (f : I  →  I )→  SO i → SO j }
-          ( s t :  snat SO SM  ) → { i j : OC } → { f :  I  →  I } →
-         { snmapsi   snmapti : SO i } →  (eqi : snmapsi ≡  snmapti ) →
-         { snmapsj   snmaptj : SO j } →  (eqj : snmapsj ≡  snmaptj )
-         → ( SM f ( snmapsi )   ≡ snmapsj )
-         → ( SM f ( snmapti )   ≡ snmaptj )
-         → SM f (snmeq s t i (eqi)) ≡ snmeq s t j (eqj)
-snmc s t refl refl refl refl = refl
-
-snat1 :   { c₂ : Level }  { I OC :  Set  c₂ } ( SO :  OC →  Set  c₂ ) ( SM : { i j :  OC  }  → (f : I  →  I )→  SO i → SO j )
-    →  ( s t :  snat SO SM   )
-    → ( eq1 : ( i : OC ) → snmap s i ≡  snmap t i )
-     → ( eq2 : ( i j : OC ) ( f : I  →  I ) →  SM {i} {j} f ( snmap s i )   ≡ snmap s j )
-     → ( eq3 : ( i j : OC ) ( f : I  →  I ) →  SM {i} {j} f ( snmap t i )   ≡ snmap t j )
-    → snat SO SM
-snat1  SO SM s t eq1 eq2 eq3 =  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 )
-   }
-
 ≡cong2 : { c c' : Level } { A B : Set  c } { C : Set  c' } { a a' : A } { b b' : B } ( f : A → B → C )
     →  a  ≡  a'
     →  b  ≡  b'
@@ -212,42 +187,6 @@
     →  f a'  ≡  g  b'
 subst2 {_} {_} {A} {B} {C} { a} {.a}  {b} {.b} f g f=g refl refl = f=g
 
-snmeqeqs  : { c₂ : Level } { I OC :  Set  c₂ } ( SO :  OC →  Set   c₂  ) ( SM : { i j :  OC  }  → (f : I  →  I )→  SO i → SO j )
-          ( s t :  snat SO SM  ) → ( i : OC ) →  ( eq1 : ( i : OC ) → snmap s i ≡  snmap t i ) →
-           snmap s i ≡ snmeq s t i  (eq1 i )
-snmeqeqs SO SM s t i eq1  = lemma  (eq1 i) refl where
-    lemma  :  { snmapsi   snmapti sm : SO i } → ( eq1 : snmapsi ≡  snmapti ) → ( snmapsi  ≡ sm ) →
-          sm  ≡ snmeq s t i  eq1
-    lemma refl refl  = refl
-
-snmeqeqt  : { c₂ : Level } { I OC :  Set  c₂ } ( SO :  OC →  Set   c₂  ) ( SM : { i j :  OC  }  → (f : I  →  I )→  SO i → SO j )
-          ( s t :  snat SO SM  ) → ( i : OC ) →  ( eq1 : ( i : OC ) → snmap s i ≡  snmap t i ) →
-           snmap t i ≡ snmeq s t i  (eq1 i )
-snmeqeqt SO SM s t i eq1  = lemma  (eq1 i) refl where
-    lemma  :  { snmapsi   snmapti sm : SO i } → ( eq1 : snmapsi ≡  snmapti ) → ( snmapti  ≡ sm ) →
-          sm  ≡ snmeq s t i  eq1
-    lemma refl refl  = refl
-
-scomm2 : { c₂ : Level } { I OC :  Set  c₂ } ( SO :  OC →  Set   c₂  ) ( SM : { i j :  OC  }  → (f : I  →  I )→  SO i → SO j )
-          ( s t :  snat SO SM  ) → ( eq1 : ( i : OC ) → snmap s i ≡  snmap t i )
-         → ( i j : OC ) → ( f :  I  →  I )
-         → SM f ( snmap s i )   ≡ snmap s j
-         → {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
-
-tcomm2 : { c₂ : Level } { I OC :  Set  c₂ } ( SO :  OC →  Set   c₂  ) ( SM : { i j :  OC  }  → (f : I  →  I )→  SO i → SO j )
-          ( s t :  snat SO SM  ) → ( eq1 : ( i : OC ) → snmap s i ≡  snmap t i )
-         → ( i j : OC ) → ( f :  I  →  I )
-         → SM f ( snmap t i )   ≡ snmap t j
-         → SM f (snmeq s t i (eq1 i)) ≡ snmeq s t j (eq1 j)
-tcomm2 SO SM s t eq1 i j f eq2 =  lemma eq2 (snmeqeqt SO SM s t i eq1) (snmeqeqt 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
-
-
 snat-cong :  { c : Level }  { I OC :  Set  c }  ( SObj :  OC →  Set  c  ) ( SMap : { i j :  OC  }  → (f : I  →  I )→  SObj i → SObj j)
          { s t :  snat SObj SMap   }
      → (( i : OC ) → snmap s i ≡  snmap t i )
@@ -255,21 +194,22 @@
      → ( ( i j : OC ) ( f : I  →  I ) →  SMap {i} {j} f ( snmap t i )   ≡ snmap t j )
      → s ≡ t
 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  }
+     record { snmap = λ i →  snmap s i ; sncommute  = λ {i} {j} f → sncommute s {i} {j} f  }
  ≡⟨
     ≡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  →  irr {!!} {!!}
+               ( extensionality Sets  ( λ  f  →  irr (subst2 {!!} {!!} {!!} {!!} (eq2 i j f ))  {!!}
              ))))))))
   ⟩
-     record { snmap = λ i →  snmap t i ; sncommute  = λ {i} {j} f → sncommute t f  }
+     record { snmap = λ i →  snmap t i ; sncommute  = λ {i} {j} f → sncommute t {i} {j} f  }
              ∎   where
                   open  import  Relation.Binary.PropositionalEquality
                   open ≡-Reasoning
 
+
 open import HomReasoning
 open NTrans