Mercurial > hg > Members > kono > Proof > category
changeset 309:e213595b845e
preinitial problem written
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 05 Jan 2014 19:16:18 +0900 |
parents | 7f00cd09274c |
children | c0439b11c7e7 |
files | freyd.agda |
diffstat | 1 files changed, 22 insertions(+), 5 deletions(-) [+] |
line wrap: on
line diff
--- a/freyd.agda Sun Jan 05 19:02:29 2014 +0900 +++ b/freyd.agda Sun Jan 05 19:16:18 2014 +0900 @@ -20,11 +20,28 @@ full→ : { a b : Obj A } { x : Hom A (FObj F a) (FObj F b) } → A [ FMap F ( FMap← x ) ≈ x ] full← : { a b : Obj A } { x : Hom A a b } → A [ FMap← ( FMap F x ) ≈ x ] -record PreInitial-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 ) +-- 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 field - pre-initial : ∀{ a : Obj A } → { a' : Obj A } → Hom A ( FObj F a' ) a - uniqueness : ∀{ a : Obj A } → { a' : Obj A } → ( f' : Hom A ( FObj F a' ) a ) → - A [ f' ≈ pre-initial {a} {a'} ] + 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 ) → + A [ f ≈ preinitial {a} {b} ] + +-- initial object +record HasInitialObject {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (i : Obj A) : Set (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where + field + initial : ( a : Obj A ) → Hom A i a + uniqueness : ( a : Obj A ) → ( f : Hom A i a ) → A [ f ≈ initial a ] + + +-- A has initial object if it has PreInitial-SmallFullSubcategory + +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 ) + (SFS : SmallFullSubcategory A F FMap← ) → + (PreInitialSmallFullSubcategory A SFS ) → { i : Obj A } → HasInitialObject A i +initialFromPreInitialFullSubcategory A F FMap← SFS PI = {!!}