# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1493373013 -32400
# Node ID 6b9737d041b492275e40af55cb4e1b55824c06d3
# Parent  761df92aa2252eac10f3a27cff48f4aaaaf090fb
one yelllow

diff -r 761df92aa225 -r 6b9737d041b4 SetsCompleteness.agda
--- a/SetsCompleteness.agda	Thu Apr 27 10:51:29 2017 +0900
+++ b/SetsCompleteness.agda	Fri Apr 28 18:50:13 2017 +0900
@@ -47,13 +47,13 @@
           prod-cong a b {c} {f} {.f} {g} {.g} refl refl = refl
 
 
-record iproduct {a} (I : Set a)  ( Product : I → Set a ) : Set a where
+record sproduct {a} (I : Set a)  ( Product : I → Set a ) : Set a where
     field
        proj : ( i : I ) → Product i
 
-open iproduct
+open sproduct
 
-iproduct1 : {  c₂ : Level} → (I : Obj (Sets {  c₂}) ) (fi : I → Obj Sets ) {q : Obj Sets} → ((i : I) → Hom Sets q (fi i)) → Hom Sets q (iproduct I fi)
+iproduct1 : {  c₂ : Level} → (I : Obj (Sets {  c₂}) ) (fi : I → Obj Sets ) {q : Obj Sets} → ((i : I) → Hom Sets q (fi i)) → Hom Sets q (sproduct I fi)
 iproduct1 I fi {q} qi x = record { proj = λ i → (qi i) x  }
 ipcx : {  c₂ : Level} → (I : Obj (Sets {  c₂})) (fi : I → Obj Sets ) {q :  Obj Sets} {qi qi' : (i : I) → Hom Sets q (fi i)} → ((i : I) → Sets [ qi i ≈ qi' i ]) → (x : q) → iproduct1 I fi qi x ≡ iproduct1 I fi qi' x
 ipcx I fi {q} {qi} {qi'} qi=qi x  = 
@@ -71,7 +71,7 @@
      → IProduct ( Sets  {  c₂} ) I
 SetsIProduct I fi = record {
        ai =  fi
-       ; iprod = iproduct I fi
+       ; iprod = sproduct I fi
        ; pi  = λ i prod  → proj prod i
        ; isIProduct = record {
               iproduct = iproduct1 I fi 
@@ -82,7 +82,7 @@
    } where
        pif=q : {q : Obj Sets} (qi : (i : I) → Hom Sets q (fi i)) {i : I} → Sets [ Sets [ (λ prod → proj prod i) o iproduct1 I fi qi ] ≈ qi i ]
        pif=q {q} qi {i} = refl
-       ip-uniqueness : {q : Obj Sets} {h : Hom Sets q (iproduct I fi)} → Sets [ iproduct1 I fi (λ i → Sets [ (λ prod → proj prod i) o h ]) ≈ h ]
+       ip-uniqueness : {q : Obj Sets} {h : Hom Sets q (sproduct I fi)} → Sets [ iproduct1 I fi (λ i → Sets [ (λ prod → proj prod i) o h ]) ≈ h ]
        ip-uniqueness = refl
 
 
@@ -183,28 +183,32 @@
 record slim  { c₂ }  { I OC :  Set  c₂ } ( sobj :  OC →  Set  c₂ ) ( smap : { i j :  OC  }  → (f : I → I ) → sobj i → sobj j ) 
       :  Set   c₂  where
    field 
-       slequ : { i j : OC } → ( f :  I → I ) →  sequ (iproduct OC sobj ) (sobj j) ( λ x → smap f ( proj x i ) ) (  λ x → proj x j )
-   snmap : OC →  Set  c₂ 
-   snmap i = sobj i
-   ipp : {i j : OC } → (f : I → I ) → iproduct OC sobj
+       slequ : { i j : OC } → ( f :  I → I ) →  sequ (sproduct OC sobj ) (sobj j) ( λ x → smap f ( proj x i ) ) (  λ x → proj x j )
+   slobj : OC →  Set  c₂ 
+   slobj i = sobj i
+   slmap : {i j : OC } →  (f : I → I ) → sobj i → sobj j
+   slmap f = smap f 
+   ipp : {i j : OC } → (f : I → I ) → sproduct OC sobj
    ipp {i} {j} f = equ ( slequ {i} {j} f )
 
 open slim
 
 lemma-equ :   {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ ) ( s : Small C I ) ( Γ : Functor C ( Sets { c₁} ))
-    {i j j' : Obj C } →　 ( f f' : I → I ) 
+    {i j i' j' : Obj C } →　 { f f' : I → I } 
     →  (se : slim (ΓObj s Γ) (ΓMap s Γ) )
-    →  proj (ipp se {i} {j} f) i ≡ proj (ipp se {i} {j'} f' ) i
-lemma-equ C I s Γ {i} {j} f f' se =   ≡cong ( λ p -> proj p i ) ( begin
-                 ipp se f 
+    →  proj (ipp se {i} {j} f) i ≡ proj (ipp se {i'} {j'} f' ) i
+lemma-equ C I s Γ {i} {j} {i'} {j'} {f} {f'} se =   ≡cong ( λ p -> proj p i ) ( begin
+                 ipp se {i} {j} f 
              ≡⟨⟩
-                 record { proj = λ i → proj (equ (slequ se f)) i }
+                 record { proj = λ x → proj (equ (slequ se f)) x }
              ≡⟨ ≡cong ( λ p → record { proj =  proj p i })  (  ≡cong ( λ QIX → record { proj = QIX } ) (  
-                extensionality Sets  ( λ  x  →  ≡cong ( λ qi →　qi x  )  refl
+                extensionality Sets  ( λ  x  →  ≡cong ( λ qi →　qi x  ) refl
               ) )) ⟩
-                 record { proj = λ i → proj (equ (slequ se f')) i }
+                ?
+             ≡⟨ ? ⟩
+                 record { proj = λ x → proj (equ (slequ se f')) x }
              ≡⟨⟩
-                 ipp se f'  
+                 ipp se {i'} {j'} f'  
              ∎  ) where
                   open  import  Relation.Binary.PropositionalEquality
                   open ≡-Reasoning
@@ -228,11 +232,11 @@
                    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)
-             ≡⟨ ≡cong ( λ g →  FMap Γ  (hom← s ( hom→ s f)) g )  ( lemma-equ  C I s Γ (\x -> x) (hom→ s f) se ) ⟩
+             ≡⟨ ≡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
              ≡⟨⟩
                   (Sets [ (λ se₁ → proj (ipp se₁ (λ x → x)) b) o FMap (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ) )) f ]) se
@@ -271,8 +275,8 @@
                   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 }
-                ≡⟨ ≡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  }
+                ≡⟨ ≡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
                   open  import  Relation.Binary.PropositionalEquality
                   open ≡-Reasoning