Mercurial > hg > Members > kono > Proof > category

comparison pullback.agda @ 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
comparison
equal deleted inserted replaced
272:5f2b8a5cc115 273:fae4bb967d76
284 limit = λ a t → limit1 a t ; 284 limit = λ a t → limit1 a t ;
285 t0f=t = λ {a t i } → t0f=t1 {a} {t} {i} ; 285 t0f=t = λ {a t i } → t0f=t1 {a} {t} {i} ;
286 limit-uniqueness = λ {a} {t} {f} t=f → limit-uniqueness1 {a} {t} {f} t=f 286 limit-uniqueness = λ {a} {t} {f} t=f → limit-uniqueness1 {a} {t} {f} t=f
287 } where 287 } where
288 limit1 : ( a : Obj A ) → ( t : NTrans I A ( K I a ) Γ ) → Hom A a a0 288 limit1 : ( a : Obj A ) → ( t : NTrans I A ( K I a ) Γ ) → Hom A a a0
289 limit1 a t = {!!} 289 limit1 a t = ?
290 t0f=t1 : { a : Obj A } → { t : NTrans I A ( K I a ) Γ } → ∀ { i : Obj I } → 290 t0f=t1 : { a : Obj A } → { t : NTrans I A ( K I a ) Γ } → ∀ { i : Obj I } →
291 A [ A [ TMap t0 i o limit1 a t ] ≈ TMap t i ] 291 A [ A [ TMap t0 i o limit1 a t ] ≈ TMap t i ]
292 t0f=t1 = {!!} 292 t0f=t1 = {!!}
293 limit-uniqueness1 : { a : Obj A } → { t : NTrans I A ( K I a ) Γ } → { f : Hom A a a0 } → ( ∀ { i : Obj I } → 293 limit-uniqueness1 : { a : Obj A } → { t : NTrans I A ( K I a ) Γ } → { f : Hom A a a0 } → ( ∀ { i : Obj I } →
294 A [ A [ TMap t0 i o f ] ≈ TMap t i ] ) → A [ limit1 a t ≈ f ] 294 A [ A [ TMap t0 i o f ] ≈ TMap t i ] ) → A [ limit1 a t ≈ f ]