# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1495668423 -32400
# Node ID b281e83521589dde65ffb83c4d1530e1e384854f
# Parent  9367813d3f6166cd12e9d31814b24bb7188a23f5
on going ...

diff -r 9367813d3f61 -r b281e8352158 SetsCompleteness.agda
--- a/SetsCompleteness.agda	Tue May 23 10:39:18 2017 +0900
+++ b/SetsCompleteness.agda	Thu May 25 08:27:03 2017 +0900
@@ -213,7 +213,7 @@
     →  (se : slim (ΓObj s Γ) (ΓMap s Γ) )
     →  proj (ipp se {i} {j} f) i ≡ proj (ipp se {i} {i} (slid C I s i) ) i
 lemma-equ' C I s Γ {i} {j} {f} se =   
-     fe=ge0 ?
+     fe=ge0 {!!}
 
 lemma-equ :   {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ ) ( s : Small C I ) ( Γ : Functor C ( Sets { c₁} ))
     {i j i' j' : Obj C } →　 { f f' : I → I } 
@@ -241,25 +241,25 @@
 Cone : {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ ) ( s : Small C I )  ( Γ : Functor C (Sets  {c₁} ) )   
     → NTrans C Sets (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ)  )) Γ
 Cone C I s  Γ =  record {
-               TMap = λ i →  λ se → proj ( ipp se {i} {i} (λ x → x) ) i
+               TMap = λ i →  λ se → proj ( ipp se {i} {i} (slid C I s i) ) i
              ; isNTrans = record { commute = commute1 }
       } where
-         commute1 :  {a b : Obj C} {f : Hom C a b} → Sets [ Sets [ FMap Γ f o (λ se → proj ( ipp se  (λ x → x) ) a) ] ≈
-                Sets [ (λ se → proj ( ipp se  (λ x → x) ) b) o FMap (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ) )) f ] ]
+         commute1 :  {a b : Obj C} {f : Hom C a b} → Sets [ Sets [ FMap Γ f o (λ se → proj ( ipp se  (slid C I s a) ) a) ] ≈
+                Sets [ (λ se → proj ( ipp se  (slid C I s b) ) b) o FMap (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ) )) f ] ]
          commute1 {a} {b} {f} =   extensionality Sets  ( λ  se  →  begin  
-                   (Sets [ FMap Γ f o (λ se₁ → proj ( ipp se  (λ x → x) ) a) ]) se
+                   (Sets [ FMap Γ f o (λ se₁ → proj ( ipp se  (slid C I s a) ) a) ]) se
              ≡⟨⟩
-                   FMap Γ f (proj ( ipp se {a} {a} (λ x → x) ) a)
-             ≡⟨  ≡cong ( λ g → FMap Γ g (proj ( ipp se {a} {a} (λ x → x) ) a))  (sym ( hom-iso s  ) ) ⟩
-                   FMap Γ  (hom← s ( hom→ s f))  (proj ( ipp se {a} {a} (λ x → x) ) a)
+                   FMap Γ f (proj ( ipp se {a} {a} (slid C I s a) ) a)
+             ≡⟨  ≡cong ( λ g → FMap Γ g (proj ( ipp se {a} {a} (slid C I s a) ) a))  (sym ( hom-iso s  ) ) ⟩
+                   FMap Γ  (hom← s ( hom→ s f))  (proj ( ipp se {a} {a} (slid C I s a) ) a)
              ≡⟨ ≡cong ( λ g →  FMap Γ  (hom← s ( hom→ s f)) g )  ( lemma-equ  C I s Γ   se ) ⟩
                    FMap Γ  (hom← s ( hom→ s f))  (proj ( ipp se {a} {b} (hom→ s f) ) a)
              ≡⟨  fe=ge0 ( slequ se (hom→ s f ) ) ⟩
                    proj (ipp se {a} {b} ( hom→ s f  )) b
              ≡⟨ sym ( lemma-equ C I s Γ se ) ⟩
-                   proj (ipp se {b} {b} (λ x → x)) b
+                   proj (ipp se {b} {b} (slid C I s b)) b
              ≡⟨⟩
-                  (Sets [ (λ se₁ → proj (ipp se₁ (λ x → x)) b) o FMap (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ) )) f ]) se
+                  (Sets [ (λ se₁ → proj (ipp se₁ (slid C I s b)) b) o FMap (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ) )) f ]) se
              ∎  ) where
                   open  import  Relation.Binary.PropositionalEquality
                   open ≡-Reasoning
@@ -294,7 +294,7 @@
                 ≡⟨   ≡cong ( λ g → record { proj = λ i → g i  } ) (  extensionality Sets  ( λ i →  sym (  ≡cong ( λ e → e x ) cif=t ) ) )  ⟩
                   record { proj = λ i → (Sets [ TMap (Cone C I s Γ) i o f ]) x }
                 ≡⟨⟩
-                  record { proj = λ i →   proj (ipp (f x) {i} {i} (λ x → x) ) i }
+                  record { proj = λ i →  proj (ipp (f x) {i} {i} (slid C I s i) ) i }
                 ≡⟨ ≡cong ( λ g →   record { proj = λ i' → g i' } ) ( extensionality Sets  ( λ  i''  → lemma-equ C I s Γ (f x)))  ⟩
                   record { proj = λ i →  proj (ipp (f x) f') i  }
                 ∎   where