# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1379853320 -32400
# Node ID fae4bb967d7624e0d9b2b9fd24b1a7bd8e545d03
# Parent  5f2b8a5cc115c64b88526290a9b8c1c769b35986
try adjoint2limit

diff -r 5f2b8a5cc115 -r fae4bb967d76 pullback.agda
--- a/pullback.agda	Sun Sep 22 21:27:03 2013 +0900
+++ b/pullback.agda	Sun Sep 22 21:35:20 2013 +0900
@@ -286,7 +286,7 @@
      limit-uniqueness =  λ {a} {t} {f} t=f → limit-uniqueness1 {a} {t} {f} t=f 
  } where
      limit1 :  ( a : Obj A ) → ( t : NTrans I A ( K I a ) Γ ) → Hom A a a0
-     limit1 a t = {!!}
+     limit1 a t = ?
      t0f=t1 :  { a : Obj A } → { t : NTrans I A ( K I a ) Γ } → ∀ { i : Obj I } →
          A [ A [ TMap t0 i o  limit1 a t ]  ≈ TMap t i ]
      t0f=t1 = {!!}