# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1493257889 -32400
# Node ID 761df92aa2252eac10f3a27cff48f4aaaaf090fb
# Parent  dbb5da4ab08fdb4b746da906e3212e73d3562f73
look like dead end

diff -r dbb5da4ab08f -r 761df92aa225 SetsCompleteness.agda
--- a/SetsCompleteness.agda	Wed Apr 26 00:55:30 2017 +0900
+++ b/SetsCompleteness.agda	Thu Apr 27 10:51:29 2017 +0900
@@ -180,7 +180,7 @@
 ΓMap  s Γ {i} {j} f = FMap Γ ( hom← s f ) 
 
 
-record slim  { c₂ }  { I OC :  Set  c₂ } ( sobj :  OC →  Set  c₂ ) ( smap : { i j :  OC  }  → (f : I → I )→  sobj i → sobj j ) 
+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 )
@@ -195,11 +195,17 @@
     {i j 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 =  begin
-                 proj ( ipp se f ) i
-             ≡⟨ {!!} ⟩
-                 proj ( ipp se f' ) i
-             ∎  where
+lemma-equ C I s Γ {i} {j} f f' se =   ≡cong ( λ p -> proj p i ) ( begin
+                 ipp se f 
+             ≡⟨⟩
+                 record { proj = λ i → proj (equ (slequ se f)) i }
+             ≡⟨ ≡cong ( λ p → record { proj =  proj p i })  (  ≡cong ( λ QIX → record { proj = QIX } ) (  
+                extensionality Sets  ( λ  x  →  ≡cong ( λ qi →　qi x  )  refl
+              ) )) ⟩
+                 record { proj = λ i → proj (equ (slequ se f')) i }
+             ≡⟨⟩
+                 ipp se f'  
+             ∎  ) where
                   open  import  Relation.Binary.PropositionalEquality
                   open ≡-Reasoning
 
@@ -222,11 +228,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 Γ {!!} {!!} se ) ⟩
+             ≡⟨ ≡cong ( λ g →  FMap Γ  (hom← s ( hom→ s f)) g )  ( lemma-equ  C I s Γ (\x -> x) (hom→ s f) 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 {!!} ⟩
+             ≡⟨  {!!}    ⟩
                    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
@@ -261,11 +267,11 @@
                      →  record { proj = λ i₁ → TMap t i₁ x }  ≡ equ (slequ (f x) f')
               uniquness2 {a} {t} {f} i j cif=t f' x = begin
                   record { proj = λ i → TMap t i x }
-                ≡⟨   ≡cong ( λ g → record { proj = λ i → g i  } ) (  extensionality Sets  ( λ  i  →  sym (  ≡cong ( λ e → e x ) cif=t ) ) )  ⟩
+                ≡⟨   ≡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) {{!!}} {{!!}} (\x -> x) ) i }
-                ≡⟨ ≡cong ( λ g →   record { proj = λ i →  g i  } ) ( extensionality Sets  ( λ  i  →  {!!}) ) ⟩
+                  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  }
                 ∎   where
                   open  import  Relation.Binary.PropositionalEquality