Mercurial > hg > Members > kono > Proof > category

changeset 310:c0439b11c7e7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
on going...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 05 Jan 2014 19:29:52 +0900
parents e213595b845e
children cf278f4d0b32
files freyd.agda
diffstat 1 files changed, 5 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/freyd.agda	Sun Jan 05 19:16:18 2014 +0900
+++ b/freyd.agda	Sun Jan 05 19:29:52 2014 +0900
@@ -42,6 +42,10 @@
 
 initialFromPreInitialFullSubcategory : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
       (F : Functor A A ) ( FMap← : { a b : Obj A } → Hom A (FObj F a) (FObj F b ) → Hom A a b )
+      -- ( lim : ( Γ : Functor I A ) → { a0 : Obj A } { t0 : NTrans I A ( K A I a0 ) Γ } → Limit A I Γ a0 t0 ) -- completeness
       (SFS : SmallFullSubcategory A F FMap← ) → 
       (PreInitialSmallFullSubcategory A SFS ) → { i : Obj A } → HasInitialObject A i
-initialFromPreInitialFullSubcategory A F  FMap← SFS PI = {!!}
+initialFromPreInitialFullSubcategory A F  FMap← SFS PI {i} = record {
+      initial = {!!} ; 
+      uniqueness  = {!!}
+    }