# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1494552305 -32400
# Node ID d3bea3ac919e164cabb93b211d9cf08623397cd9
# Parent  c78df4c0453c62a53240623820ba77a150fb1ff0
on going ...

diff -r c78df4c0453c -r d3bea3ac919e SetsCompleteness.agda
--- a/SetsCompleteness.agda	Thu May 11 17:06:27 2017 +0900
+++ b/SetsCompleteness.agda	Fri May 12 10:25:05 2017 +0900
@@ -180,7 +180,7 @@
                 ( sobj :  OC →  Set  c₂ ) ( smap : { i j :  OC  }  → (f : I → I ) → sobj i → sobj j ) 
       :  Set   c₂  where
    field 
-       slequ : ( e : OC → sproduct OC sobj  )  (i j : OC) (f :  I → I  ) → sequ OC (sobj j) (λ x →  smap f (proj (e x) i) ) (λ x → proj (e x) j )
+       slequ : (i j : OC) (f :  I → I  ) → sequ (sproduct OC sobj) (sobj j) (λ x →  smap f (proj x i) ) (λ x → proj x j )
        slprod :  sproduct OC  sobj 
 
 open slim
@@ -188,36 +188,30 @@
 open import HomReasoning
 open NTrans
 
-cequ :  {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ ) ( s : Small C I )  ( Γ : Functor C (Sets  {c₁} ) )
-    → ( e : Hom Sets ( slim (ΓObj s Γ) (ΓMap s Γ)) (sproduct (Obj C) (ΓObj s  Γ) ))   (se : slim (ΓObj s Γ) (ΓMap s Γ)  ) → (b : Obj C )  
-    → sproduct (Obj C) (ΓObj s  Γ)
-cequ C I s Γ e se b = equ {_} {sproduct (Obj C) (ΓObj s Γ)}  {ΓObj s Γ b} {λ x → proj x b }  {λ x → proj x b} (elem (e se) refl)
 cone-equ :  {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ ) ( s : Small C I )  ( Γ : Functor C (Sets  {c₁} ) )
-    → ( e : Hom Sets ( slim (ΓObj s Γ) (ΓMap s Γ)  ) (sproduct (Obj C) (ΓObj s  Γ)  )   )
     →  (a b : Obj C) (f : I → I ) → (se : slim (ΓObj s Γ) (ΓMap s Γ)  ) 
-    → sequ (slim (ΓObj s Γ) (ΓMap s Γ)) (FObj Γ b) (λ x →  FMap Γ (hom← s f) (proj (e x) a) ) (λ x → proj (e x) b )
-cone-equ C I s Γ e a b f se = elem se ( fe=ge0 (slequ se ( λ x → record { proj = λ i → proj ( e se ) i  } )  a b f ) )
+    → sequ (slim (ΓObj s Γ) (ΓMap s Γ)) (FObj Γ b) (λ x →  FMap Γ (hom← s f) (proj (slprod x) a) ) (λ x → proj (slprod x) b )
+cone-equ C I s Γ a b f se = elem se {!!} -- (( fe=ge0 (slequ se  a b f  )) )
 
 Cone : {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ ) ( s : Small C I )  ( Γ : Functor C (Sets  {c₁} ) )   
-    → ( e : Hom Sets ( slim (ΓObj s Γ) (ΓMap s Γ)  ) (sproduct (Obj C) (ΓObj s  Γ)  ) )
     → NTrans C Sets (K Sets C ( slim (ΓObj s Γ) (ΓMap s Γ)))  Γ
-Cone C I s  Γ e  =  record {
+Cone C I s  Γ =  record {
                TMap = λ i →  λ se → proj ( equ {_} { sproduct (Obj C) (ΓObj s  Γ)}  {FObj Γ i}
-                     {λ x → proj x i} {λ x → proj x i} (elem (e se ) refl )) i
+                     {λ x → proj x i} {λ x → proj x i} (elem (slprod se) refl )) i
              ; isNTrans = record { commute = commute1 }
       } where
-         commute1 :  {a b : Obj C} {f : Hom C a b} → Sets [ Sets [ FMap Γ f o (λ se → proj (cequ C I s Γ e se b) a) ]
-              ≈ Sets [ (λ se → proj (cequ C I s Γ e se b) 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 (slprod se) a) ]
+              ≈ Sets [ (λ se → proj (slprod se) 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 (cequ C I s Γ e se b) a) ]) se
+                 (Sets [ FMap Γ f o (λ se → proj (slprod se) a) ]) se
              ≡⟨⟩
-                  FMap Γ f (proj (e se) a )
-             ≡⟨  ≡cong ( λ g → FMap Γ g (proj (e se) a))  (sym ( hom-iso s  ) ) ⟩
-                   FMap Γ  (hom← s ( hom→ s f))  (proj (e se) a)
-             ≡⟨  fe=ge0 (cone-equ  C I s Γ e a b ( hom→ s f) se ) ⟩
-                  proj (e se) b 
+                  FMap Γ f (proj (slprod se) a )
+             ≡⟨  ≡cong ( λ g → FMap Γ g (proj (slprod se) a))  (sym ( hom-iso s  ) ) ⟩
+                   FMap Γ  (hom← s ( hom→ s f))  (proj (slprod se) a)
+             ≡⟨  fe=ge0 (cone-equ  C I s Γ a b ( hom→ s f) se ) ⟩
+                  proj (slprod se) b 
              ≡⟨⟩
-                  (Sets [ (λ se → proj (cequ C I s Γ e se b) b) o FMap (K Sets C ( slim (ΓObj s Γ) (ΓMap s Γ)  )) f ]) se
+                  (Sets [ (λ se → proj (slprod se) b) o FMap (K Sets C ( slim (ΓObj s Γ) (ΓMap s Γ)  )) f ]) se
              ∎  ) where
                   open  import  Relation.Binary.PropositionalEquality
                   open ≡-Reasoning
@@ -227,17 +221,16 @@
     → Limit Sets C Γ
 SetsLimit { c₂} C I s Γ = record { 
            a0 =  slim  (ΓObj s Γ) (ΓMap s Γ) 
-         ; t0 = Cone C I s Γ ( λ se → slprod se )
+         ; t0 = Cone C I s Γ 
          ; isLimit = record {
                limit  = limit1
              ; t0f=t = λ {a t i } → {!!}
              ; limit-uniqueness  =  λ {a t i }  → {!!}
           }
        }  where
-          comm2 : ( e : Hom Sets ( slim (ΓObj s Γ) (ΓMap s Γ)  )  (sproduct (Obj C) (ΓObj s  Γ)  ) ) {i j : Obj C } ( f : I → I ) 
-             → (p : sproduct (Obj C) (ΓObj s  Γ) )
-             → ΓMap s Γ f (proj p i) ≡ proj p j
-          comm2  e {i} {j} f p = {!!}
+          --    ( e : Obj C  → sproduct (Obj C) sobj  )
+          --    sequ (Obj C) (ΓObj s Γ j) (λ x₁ → ΓMap s Γ f (proj (e x₁) i)) (λ x₁ → proj (e x₁) j)
           limit1 : (a : Obj Sets) → NTrans C Sets (K Sets C a) Γ → Hom Sets a (slim (ΓObj s Γ) (ΓMap s Γ)) 
-          limit1 a t = λ x →  record { slequ = λ e i j f → ?
+          limit1 a t = λ x →  record { slequ = λ i j f →  k (λ p → 
+                iproduct1 (Obj C) (ΓObj s Γ) (TMap t) x) (extensionality Sets  ( λ y → ? )) x 
                ; slprod = record { proj = λ i → TMap t i x } }