Mercurial > hg > Members > kono > Proof > category

changeset 308:7f00cd09274c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
pre-initial
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 05 Jan 2014 19:02:29 +0900
parents 9872bddec072
children e213595b845e
files freyd.agda
diffstat 1 files changed, 8 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/freyd.agda	Sun Jan 05 18:51:44 2014 +0900
+++ b/freyd.agda	Sun Jan 05 19:02:29 2014 +0900
@@ -20,3 +20,11 @@
       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 )
+      (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'} ]
+