--- a/freyd.agda	Sun Jan 05 10:36:11 2014 +0900
+++ b/freyd.agda	Sun Jan 05 18:51:44 2014 +0900
@@ -5,21 +5,18 @@
 module freyd {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
   where
 
+open import cat-utility
 open import Relation.Binary.Core
+open Functor
 
 -- C is small full subcategory of A
 
-record SmallFullSubcategory {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( f : Obj A → Obj A ) : Set (ℓ ⊔ (c₁ ⊔ c₂)) where
-   ObjC : Set  c₁
-   ObjC = Category.Category.Obj A
-   C : Category c₁ c₂ ℓ
-   C = record { Obj = ObjC
-         ; Hom = Category.Category.Hom A
-         ; _o_ = Category.Category._o_ A
-         ; _≈_ = Category.Category._≈_ A
-         ; Id  = Category.Category.Id  A
-         ; isCategory = Category.isCategory A
-       } 
+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 )
+           : Set  (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where
    field
-      ≈→≡ : {a b : Obj C } { x y : Hom C a b } →  (x≈y : C [ x ≈ y  ]) → x ≡ y 
+      ≈→≡ : {a b : Obj A } →  { x y : Hom A (FObj F a) (FObj F b) } → 
+                (x≈y : A [ FMap F x ≈ FMap F y  ]) → FMap F x ≡ FMap F y   -- co-comain of FMap is local small
+      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 ]