# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1494564331 -32400
# Node ID 11b5eeb4a9e7febfacfb6ccedb17cf340ddc6c44
# Parent  d3bea3ac919e164cabb93b211d9cf08623397cd9
fix

diff -r d3bea3ac919e -r 11b5eeb4a9e7 SetsCompleteness.agda
--- a/SetsCompleteness.agda	Fri May 12 10:25:05 2017 +0900
+++ b/SetsCompleteness.agda	Fri May 12 13:45:31 2017 +0900
@@ -232,5 +232,11 @@
           --    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 = λ i j f →  k (λ p → 
-                iproduct1 (Obj C) (ΓObj s Γ) (TMap t) x) (extensionality Sets  ( λ y → ? )) x 
+                iproduct1 (Obj C) (ΓObj s Γ) (TMap t) x) ( begin
+                         (λ x₁ → ΓMap s Γ f (proj x₁ i)) o (λ p → iproduct1 (Obj C) (ΓObj s Γ) (TMap t) x)
+                      ≈⟨ car  (nat t)  ⟩
+                         (λ x₁ → proj x₁ j) o (λ p → iproduct1 (Obj C) (ΓObj s Γ) (TMap t) x)
+                      ∎ 
+                    ) x
                ; slprod = record { proj = λ i → TMap t i x } } 
+                        where open ≈-Reasoning (Sets { c₂})