Mercurial > hg > Members > kono > Proof > category

changeset 273:fae4bb967d76

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
try adjoint2limit
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 22 Sep 2013 21:35:20 +0900
parents 5f2b8a5cc115
children 1b651faa2391
files pullback.agda
diffstat 1 files changed, 1 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- 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 = {!!}