Mercurial > hg > Members > kono > Proof > category

changeset 459:9d24fb809746

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
freyd trbouled again
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 02 Mar 2017 20:22:42 +0900
parents fd79b6d9f350
children 961c236807f1
files freyd.agda
diffstat 1 files changed, 8 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/freyd.agda	Thu Mar 02 19:04:04 2017 +0900
+++ b/freyd.agda	Thu Mar 02 20:22:42 2017 +0900
@@ -58,14 +58,16 @@
       F = SFSF SFS   
       FMap← : { a b : Obj A } → Hom A (FObj F a) (FObj F b ) → Hom A a b 
       FMap←  = SFSFMap←  SFS
-      lim : ( Γ : Functor A A ) → Limit A A Γ (limit-c comp Γ)  (limit-u comp Γ)
-      lim Γ =  isLimit comp Γ 
+      a0 : Obj A
+      a0 = limit-c comp F
+      uΓ : ( Γ : Functor A A ) →  NTrans A A (K A A (limit-c comp Γ)) Γ
+      uΓ Γ = {!!}
+      lim : ( Γ : Functor A A ) → Limit A A Γ (limit-c comp Γ) (uΓ Γ)
+      lim Γ =  isLimit comp Γ (uΓ Γ)
+      u : NTrans A A (K A A a0) F
+      u = T0 ( lim F )
       equ : {a b : Obj A} → (f g : Hom A a b)  → IsEqualizer A (equalizer-e comp f g ) f g
       equ f g = Complete.isEqualizer comp f g 
-      a0 : Obj A
-      a0 = limit-c comp F
-      u : NTrans A A (K A A a0) F
-      u = limit-u comp F
       ep : {a b : Obj A} → {f g : Hom A a b}  → Obj A 
       ep {a} {b} {f} {g} = equalizer-p comp f g
       ee :  {a b : Obj A} → {f g : Hom A a b}  → Hom A (ep {a} {b} {f} {g} ) a