Mercurial > hg > Members > kono > Proof > category

changeset 311:cf278f4d0b32

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:34:11 +0900
parents c0439b11c7e7
children 702adc45704f
files freyd.agda
diffstat 1 files changed, 4 insertions(+), 5 deletions(-) [+]
line wrap: on
line diff
--- a/freyd.agda	Sun Jan 05 19:29:52 2014 +0900
+++ b/freyd.agda	Sun Jan 05 19:34:11 2014 +0900
@@ -9,7 +9,7 @@
 open import Relation.Binary.Core
 open Functor
 
--- C is small full subcategory of A
+-- C is small full subcategory of A ( C is image of F )
 
 record SmallFullSubcategory {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 )
@@ -22,9 +22,8 @@
 
 -- pre-initial
 
-record PreInitialSmallFullSubcategory {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 }
-      (SFS : SmallFullSubcategory A F FMap← ) : Set  (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where
+record PreInitial {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
+      (F : Functor A A )  : Set  (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where
    field
       preinitial : ∀{  a : Obj A } → { b : Obj A } →  Hom A ( FObj F b ) a 
       uniqueness  : ∀{  a : Obj A } → { b : Obj A } →  ( f : Hom A ( FObj F b ) a ) →
@@ -44,7 +43,7 @@
       (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
+      (PreInitial A F ) → { i : Obj A } → HasInitialObject A i
 initialFromPreInitialFullSubcategory A F  FMap← SFS PI {i} = record {
       initial = {!!} ; 
       uniqueness  = {!!}