--- a/freyd.agda	Sun Jan 05 08:46:31 2014 +0900
+++ b/freyd.agda	Sun Jan 05 09:52:13 2014 +0900
@@ -8,7 +8,14 @@
 
 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 _⊆_ _⊇_ 
 
--- record SmallCategory 
+_⊆_ : ∀ {ℓ₁ ℓ₂} → Set ℓ₁ → Set ℓ₂ → Set _
+P ⊆ Q = ∀ {x : P} →  {y : Q } → x ≡ y
+
+_⊇_ : ∀ {ℓ₁ ℓ₂} → Set ℓ₁ → Set ℓ₂ → Set _
+Q ⊇ P = ∀ {x : P} →  {y : Q } → x ≡ y
+