# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1388916149 -32400
# Node ID 7f00cd09274c4966ec1bad7e1d616716cf600c84
# Parent  9872bddec0728b60b5dadfa91b955a6808396f4f
pre-initial

diff -r 9872bddec072 -r 7f00cd09274c freyd.agda
--- 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'} ]
+