# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1493040419 -32400
# Node ID 46e4177546017f6e9eb394b86e3ecf68f2cfd80c
# Parent  143de0e3eb60be951ffafd57d2df93bd5546beeb
fix

diff -r 143de0e3eb60 -r 46e417754601 SetsCompleteness.agda
--- a/SetsCompleteness.agda	Mon Apr 24 21:08:57 2017 +0900
+++ b/SetsCompleteness.agda	Mon Apr 24 22:26:59 2017 +0900
@@ -223,7 +223,7 @@
              ≡⟨⟩
                    FMap Γ f (snmap (equ (slequ se (λ x → x))) a)
              ≡⟨  ≡cong ( λ g → FMap Γ g (snmap (equ (slequ se (λ x → x))) a))  (sym ( hom-iso s  ) ) ⟩
-                   FMap Γ  (hom← s ( hom→ s f))  (snmap (equ {_} {_} {_} {_} {_} (slequ se {a} {a} (λ x → x))) a)
+                   FMap Γ  (hom← s ( hom→ s f))  (snmap (equ (slequ se {a} {a} (λ x → x))) a)
              ≡⟨ ≡cong ( λ g →  FMap Γ  (hom← s ( hom→ s f)) g )  ( lemma-equ C I s Γ  )   ⟩
                    FMap Γ  (hom← s ( hom→ s f))  (snmap (equ (slequ se (hom→ s f ))) a)
              ≡⟨  fe=ge0 ( slequ se (hom→ s f ) ) ⟩
@@ -259,16 +259,15 @@
               uniquness2 : {a : Obj Sets} {t : NTrans C Sets (K Sets C a) Γ} {f : Hom Sets a (slim (ΓObj s Γ) (ΓMap s Γ) )} 
                      →  ( i j : Obj C  ) →
                     ({i  : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ) i o f ] ≈ TMap t i ]) →  (f' : I → I ) →  (x : a ) 
-                     →  equ {_} {_} {slobj (f x) j }  {{!!}} {{!!}}
-                         (elem (record { snmap = λ i₁ → TMap t i₁ x }) (limit2 a t {i} {j} f' x)) ≡ equ (slequ (f x) f')
+                     →  record { snmap = λ i₁ → TMap t i₁ x }  ≡ equ (slequ (f x) f')
               uniquness2 {a} {t} {f} i j cif=t f' x = begin
-                  record { snmap = λ i₁ → TMap t i₁ x }
+                  record { snmap = λ i → TMap t i x }
                 ≡⟨   ≡cong ( λ g → record { snmap = λ i → g i  } ) (  extensionality Sets  ( λ  i  →  sym (  ≡cong ( λ e → e x ) cif=t ) ) )  ⟩
                   record { snmap = λ i → (Sets [ TMap (Cone C I s Γ) i o f ]) x }
                 ≡⟨⟩
                   record { snmap = λ i →   snmap (equ (slequ (f x) {i} {i} (λ x → x )) ) i }
                 ≡⟨ ≡cong ( λ g →   record { snmap = λ i →  g i  } ) (  extensionality Sets  ( λ  i  → lemma-equ C I s Γ ))  ⟩
-                  record { snmap = λ i₁ →  snmap (equ (slequ (f x) f')) i₁  }
+                  record { snmap = λ i →  snmap (equ (slequ (f x) f')) i  }
                 ∎   where
                   open  import  Relation.Binary.PropositionalEquality
                   open ≡-Reasoning