# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1492942624 -32400
# Node ID 8b18361e6ca98cbc0dd25e110ff775cce579fb6f
# Parent  14483d9d604c747f1447616e9f52d73513dad71d
try id equalizer

diff -r 14483d9d604c -r 8b18361e6ca9 SetsCompleteness.agda
--- a/SetsCompleteness.agda	Mon Apr 10 12:16:01 2017 +0900
+++ b/SetsCompleteness.agda	Sun Apr 23 19:17:04 2017 +0900
@@ -112,14 +112,19 @@
 elm-cong :  {  c₂ : Level}  →  {a b : Obj (Sets {c₂}) }  {f g : Hom (Sets {c₂}) a b} →   (x y : sequ a b f g) → equ x ≡ equ y →  x  ≡ y
 elm-cong ( elem x eq  ) (elem .x eq' ) refl   =  ≡cong ( λ ee → elem x ee ) ( irr eq eq' )
 
-fe=ge  : {  c₂ : Level}  →  {a b : Obj (Sets {c₂}) }  {f g : Hom (Sets {c₂}) a b} →  Sets [ Sets [ f o (λ e → equ e ) ] ≈ Sets [ g o (λ e → equ e ) ] ]
+fe=ge  : {  c₂ : Level}  →  {a b : Obj (Sets {c₂}) }  {f g : Hom (Sets {c₂}) a b} 
+     →  Sets [ Sets [ f o (λ e → equ {_} {a} {b} {f} {g} e ) ] ≈ Sets [ g o (λ e → equ e ) ] ]
 fe=ge  =  extensionality Sets (fe=ge0 ) 
 k : {  c₂ : Level}  →  {a b : Obj (Sets {c₂}) }  {f g : Hom (Sets {c₂}) a b} →  {d : Obj Sets} (h : Hom Sets d a) 
      → Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ] → Hom Sets d (sequ a b f g)
 k {_} {_} {_} {_} {_} {d} h eq = λ x → elem  (h x) ( ≡cong ( λ y → y x ) eq )
-ek=h : {  c₂ : Level}  →  {a b : Obj (Sets {c₂}) }  {f g : Hom (Sets {c₂}) a b} →  {d : Obj Sets} {h : Hom Sets d a} {eq : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ]} → Sets [ Sets [ (λ e → equ e )  o k h eq ] ≈ h ]
+ek=h : {  c₂ : Level}  →  {a b : Obj (Sets {c₂}) }  {f g : Hom (Sets {c₂}) a b} →  {d : Obj Sets} {h : Hom Sets d a} {eq : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ]} → Sets [ Sets [ (λ e → equ {_} {a} {b} {f} {g} e )  o k h eq ] ≈ h ]
 ek=h {_} {_} {_} {_} {_} {d} {h} {eq} = refl 
 
+lemma-equ : {  c₂ : Level} {a b b' : Obj (Sets {c₂}) } { f g : Hom (Sets {c₂}) a b } { f' g' : Hom (Sets {c₂}) a b' }
+          (s : sequ a b f g )  ( t : sequ a b' f' g' )    →   equ s ≡ equ t
+lemma-equ ( elem x eq ) ( elem y eq')  =  {!!}
+
 open sequ
 
 --           equalizer-c = sequ a b f g
@@ -135,7 +140,7 @@
            injection :  { c₂ : Level  } {a b  : Obj (Sets { c₂})} (f  : Hom Sets a b) → Set c₂
            injection f =  ∀ x y  → f x ≡ f y →  x  ≡ y
            lemma5 :   {d : Obj Sets} {h : Hom Sets d a} {fh=gh : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ]} {k' : Hom Sets d (sequ a b f g)} →
-                Sets [ Sets [ (λ e → equ e) o k' ] ≈ h ] → (x : d ) → equ (k h fh=gh x) ≡ equ (k' x)
+                Sets [ Sets [ (λ e → equ e) o k' ] ≈ h ] → (x : d ) → equ {_} {a} {b} {f} {g} (k h fh=gh x) ≡ equ (k' x)
            lemma5 refl  x  = refl   -- somehow this is not equal to lemma1
            uniqueness :   {d : Obj Sets} {h : Hom Sets d a} {fh=gh : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ]} {k' : Hom Sets d (sequ a b f g)} →
                 Sets [ Sets [ (λ e → equ e) o k' ] ≈ h ] → Sets [ k h fh=gh  ≈ k' ]
@@ -187,8 +192,7 @@
 record snequ  { c₂ }  { I OC :  Set  c₂ } ( sobj :  OC →  Set  c₂ ) ( smap : { i j :  OC  }  → (f : I → I )→  sobj i → sobj j ) 
       :  Set   c₂  where
    field 
-       sn :  snproj sobj smap
-       snequ1 : { i j : OC } → ( f :  I → I ) →  sequ (sobj i) (sobj j) ( λ x → smap f ( snmap sn i ) ) (  λ x → snmap sn j )
+       snequ1 : { i j : OC } → ( f :  I → I ) →  sequ (snproj sobj smap ) (sobj j) ( λ x → smap f ( snmap x i ) ) (  λ x → snmap x j )
 
 open snequ
 
@@ -198,66 +202,39 @@
 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 (snequ (ΓObj s Γ) (ΓMap s Γ) )) Γ
 Cone C I s  Γ =  record {
-               TMap = λ i →  λ se → snmap ( sn se ) i
-             ; isNTrans = record { commute = comm1 }
+               TMap = λ i →  λ se → snmap (equ (snequ1 se {i} {i} (λ x → x )) ) i
+             ; isNTrans = record { commute = {!!} }
       } where
-    comm1 :  {a b : Obj C} {f : Hom C a b} →
-        Sets [ Sets [ FMap Γ f o (λ se → snmap (sn se) a) ] ≈
-        Sets [ (λ se → snmap (sn se) b) o FMap (K Sets C (snequ (ΓObj s Γ) (ΓMap s Γ))) f ] ]
-    comm1 {a} {b} {f} =   extensionality Sets  ( λ  se  →  begin  
-                  FMap Γ f (snmap (sn se) a)
-             ≡⟨ ≡cong ( λ f → FMap Γ f ( snmap (sn se) a )) (sym ( hom-iso s ))  ⟩
-                  FMap Γ (hom← s ( hom→ s f)) (snmap (sn se) a)
-             ≡⟨ fe=ge0 ( snequ1 se (hom→ s f ) )  ⟩
-                  snmap (sn se) b
+         commute1 :  {a b : Obj C} {f : Hom C a b} → Sets [ Sets [ FMap Γ f o (λ se → snmap (equ (snequ1 se {a} {a} (λ x → x))) a) ] ≈
+                Sets [ (λ se → snmap (equ (snequ1 se {b} {b} (λ x → x))) b) o FMap (K Sets C (snequ (ΓObj s Γ) (ΓMap s Γ))) f ] ]
+         commute1 {a} {b} {f} =   extensionality Sets  ( λ  se  →  begin  
+                   (Sets [ FMap Γ f o (λ se₁ → snmap (equ (snequ1 se₁ (λ x → x))) a) ]) se
+             ≡⟨⟩
+                   FMap Γ f (snmap (equ (snequ1 se (λ x → x))) a)
+             ≡⟨ {!!} ⟩
+                   FMap Γ  (hom← s ( hom→ s f))  (snmap (equ (snequ1 se {a} {a} (λ x → x))) a)
+             ≡⟨ {!!} ⟩
+                   FMap Γ  (hom← s ( hom→ s f))  (snmap (equ (snequ1 se (hom→ s f ))) a)
+             ≡⟨  fe=ge0 ( snequ1 se (hom→ s f ) ) ⟩
+                   snmap (equ (snequ1 se ( hom→ s f ) )) b
+             ≡⟨ {!!} ⟩
+                   snmap (equ (snequ1 se (λ x → x))) b
+             ≡⟨⟩
+                  (Sets [ (λ se₁ → snmap (equ (snequ1 se₁ (λ x → x))) b) o FMap (K Sets C (snequ (ΓObj s Γ) (ΓMap s Γ))) f ]) se
              ∎  ) where
                   open  import  Relation.Binary.PropositionalEquality
                   open ≡-Reasoning
 
+
+
 SetsLimit : {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ ) ( small : Small C I ) ( Γ : Functor C (Sets  {c₁} ) ) 
     → Limit Sets C Γ
 SetsLimit { c₂} C I s Γ = record { 
            a0 =  snequ  (ΓObj s Γ) (ΓMap s Γ)  
          ; t0 = Cone C I s Γ 
          ; isLimit = record {
-               limit  = limit1
-             ; t0f=t = λ {a t i } → t0f=t {a} {t} {i}
-             ; limit-uniqueness  =  λ {a t i }  → limit-uniqueness   {a} {t} {i}
+               limit  =  {!!}
+             ; t0f=t = λ {a t i } → {!!}
+             ; limit-uniqueness  =  λ {a t i }  → {!!}
           }
        }  where
-          setprod : {a : Obj Sets} → NTrans C Sets (K Sets C a) Γ → (x : a ) → snproj  (ΓObj s Γ) (ΓMap s Γ)
-          setprod t x  = record { snmap = λ i → TMap t i x }
-          comm3 : { a : Obj Sets } {x : a } {i j : Obj C} (t : NTrans C Sets (K Sets C a) Γ) (f : I → I ) 
-              →  Sets [ Sets [ (λ x₁ → ΓMap s Γ f (snmap (setprod t x) i)) o TMap t i ] ≈ Sets [ (λ x₁ → snmap (setprod t x) j) o TMap t i ] ]
-          comm3 {a} {x} t f =   {!!}
-          limit1 : (a : Obj Sets) → NTrans C Sets (K Sets C a) Γ → Hom Sets a (snequ (ΓObj s Γ) (ΓMap s Γ)) 
-          limit1 a t = λ ( x : a ) →  record {
-                sn =  setprod t x
-                ; snequ1 = λ {i} {j} f → k (TMap t i ) (comm3 t f ) x 
-            }
-          t0f=t : {a : Obj Sets} {t : NTrans C Sets (K Sets C a) Γ} {i : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ ) i o limit1 a t ] ≈ TMap t i ]
-          t0f=t {a} {t} {i} =  extensionality Sets  ( λ  x  →  begin
-                 ( Sets [ TMap (Cone C I s Γ ) i o limit1 a t ]) x
-             ≡⟨⟩
-                 TMap t i x
-             ∎  ) where
-                  open  import  Relation.Binary.PropositionalEquality
-                  open ≡-Reasoning
-          limit-uniqueness : {a : Obj Sets} {t : NTrans C Sets (K Sets C a) Γ} {f : Hom Sets a (snequ (ΓObj s Γ) (ΓMap s Γ) )} →
-                ({i : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ ) i o f ] ≈ TMap t i ]) → Sets [ limit1 a t ≈ f ]
-          limit-uniqueness {a} {t} {f} cif=t = extensionality Sets  ( λ  x  →  begin
-                  limit1 a t x
-             ≡⟨⟩
-                  record { sn =  setprod t x  ; snequ1 = λ {i} f' → k ( TMap t i ) (comm3 {a} {x} t f' ) x }
-             ≡⟨ ≡cong2 {!!} {!!} {!!}  ⟩
-                  record { sn = sn ( f x ) ; snequ1 = λ {i} {j} f' →  ( snequ1 (f x ) f' )  }
-             ≡⟨⟩
-                  f x
-             ∎  ) where
-                  open  import  Relation.Binary.PropositionalEquality
-                  open ≡-Reasoning
-                  snmap-cong : ( e : snequ  (ΓObj s Γ) (ΓMap s Γ) ) {i : Obj C } { f g : I → I } 
-                        →   {!!} -- snmap ( equ ( snequ1 e  f)) i ≡  snmap ( equ ( snequ1 e  g)) i
-                  snmap-cong e {i} =  ≡cong ( λ s → snmap s i ) refl
-                  k-cong : { i j : Obj C } ( f' : I → I )  ( x : a ) →   k ( TMap t i ) {!!} x ≡  snequ1 (f x) f' 
-                  k-cong {i} {j} f' x =  {!!}