# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1508682990 -32400
# Node ID 9e8276b89cd0c625bd594231ca3c447650a8bdab
# Parent  855e497a9c8f0cd7ea2199e138131a8bc36ee0c5
...

diff -r 855e497a9c8f -r 9e8276b89cd0 SetsCompleteness.agda
--- a/SetsCompleteness.agda	Sun Oct 22 22:42:56 2017 +0900
+++ b/SetsCompleteness.agda	Sun Oct 22 23:36:30 2017 +0900
@@ -183,6 +183,7 @@
 
 open import Relation.Binary.HeterogeneousEquality as HE renaming ( cong to cong' ; sym to sym' ; subst₂ to subst₂' ; Extensionality to Extensionality' )
     using (_≅_;refl)
+postulate ≅extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → HE.Extensionality c₂ c₂
 
 snat-cong : {c : Level}
                 {I OC : Set c}
@@ -232,7 +233,7 @@
        }  where
           comm2 : { a : Obj Sets } {x : a } {i j : Obj C} (t : NTrans C Sets (K Sets C a) Γ) (f : I)
              → ΓMap s Γ f (TMap t i x) ≡ TMap t j x
-          comm2 {a} {x} t f =  ≡cong ( λ f → f x ) ( IsNTrans.commute ( isNTrans t ) )
+          comm2 {a} {x} t f =  ≡cong ( λ h → h x ) ( IsNTrans.commute ( isNTrans t ) )
           limit1 : (a : Obj Sets) → NTrans C Sets (K Sets C a) Γ → Hom Sets a (snat (ΓObj s Γ) (ΓMap s Γ))
           limit1 a t = λ x →  record { snmap = λ i →  ( TMap t i ) x ;
               sncommute = λ i j f → comm2 t f }
@@ -251,20 +252,20 @@
              ≡⟨⟩
                   record { snmap = λ i →  ( TMap t i ) x ; sncommute = λ i j f → comm2 t f }
              ≡⟨ snat-cong (limit1 a t x) (f x ) ( extensionality Sets  ( λ  i  →  eq1 x i )) (eq2 x ) ⟩
-                  record { snmap = λ i →  snmap  (f x ) i  ; sncommute = λ i j f' → sncommute (f x ) i j f'  }
+                  record { snmap = λ i →  snmap  (f x ) i  ; sncommute = λ i j g → sncommute (f x ) i j g  }
              ≡⟨⟩
                   f x
              ∎  ) where
                   open  import  Relation.Binary.PropositionalEquality
-                  postulate ≅extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → HE.Extensionality c₂ c₂
                   open ≡-Reasoning
                   eq1 : (x : a ) (i : Obj C) → TMap t i x ≡ snmap (f x) i
                   eq1 x i = sym ( ≡cong ( λ f → f x ) cif=t  )
-                  eq2' : ( x : a) → (λ i j f₁ → smap0 (limit1 a t x) f₁ (snmap (limit1 a t x) i) ≡ snmap (limit1 a t x) j)
-                        ≅ (λ i j  f₁ → smap0 (f x) f₁ (snmap (f x) i) ≡ snmap (f x) j)
-                  eq2' x = {!!}
                   irr≅ : { c₂ : Level}  {d : Set c₂ }  { x y : d } ( eq eq' :  x  ≡ y ) → eq ≅ eq'
                   irr≅ refl refl = refl
+                  eq3 :  ( x : a)  ( i j : Obj C ) ( g : I ) → ≡cong ( λ h → h x ) ( IsNTrans.commute ( isNTrans t ) {i} {j} {hom← s g }  )
+                      ≅  sncommute (f x) i j g
+                  eq3 x i j g = {!!}
                   -- eq2 :  ( x : a) → sncommute (limit1 a t x) ≅ sncommute (f x)
-                  eq2 :  ( x : a) →  ( λ i j f → ≡cong ( λ f → f x ) ( IsNTrans.commute ( isNTrans t )))  ≅ sncommute (f x)
+                  eq2 :  ( x : a) →  ( λ i j g → ≡cong ( λ h → h x ) ( IsNTrans.commute ( isNTrans t ) {i} {j} {hom← s g } ))
+                      ≅ ( λ i j g →  sncommute (f x) i j g )
                   eq2 x = {!!}