--- a/freyd.agda	Sun Jan 05 09:52:13 2014 +0900
+++ b/freyd.agda	Sun Jan 05 10:36:11 2014 +0900
@@ -3,19 +3,23 @@
 open import Category.Sets
 
 module freyd {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
-     (C : Category zero zero zero )
   where
 
 open import Relation.Binary.Core
 
--- C is locally small
-postulate ≈→≡ : {a b : Obj C } { x y : Hom C a b } →  (x≈y : C [ x ≈ y  ]) → x ≡ y
-
-infix 4 _⊆_ _⊇_ 
+-- C is small full subcategory of A
 
-_⊆_ : ∀ {ℓ₁ ℓ₂} → Set ℓ₁ → Set ℓ₂ → Set _
-P ⊆ Q = ∀ {x : P} →  {y : Q } → x ≡ y
+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
+       } 
+   field
+      ≈→≡ : {a b : Obj C } { x y : Hom C a b } →  (x≈y : C [ x ≈ y  ]) → x ≡ y 
 
-_⊇_ : ∀ {ℓ₁ ℓ₂} → Set ℓ₁ → Set ℓ₂ → Set _
-Q ⊇ P = ∀ {x : P} →  {y : Q } → x ≡ y
-