--- a/limit-to.agda	Wed Dec 24 22:16:20 2014 +0900
+++ b/limit-to.agda	Wed Apr 01 17:37:04 2015 +0900
@@ -20,46 +20,83 @@
 ---       ------>
 ---          g
 
+data  _∨_  {c₁} (A B : Set c₁): Set c₁ where
+        or1 :  A → A ∨ B
+        or2 :  B → A ∨ B
+
+
+record TwoSet {c₁} (A : Set c₁): Set (suc c₁) where
+    field
+            a0 : A
+            a1 : A
+            element : (x : A) → ( x ≡ a0) ∨ (x ≡ a1 )
+            
+
 data Two {c₁}  : Set c₁ where
    t0 : Two 
    t1 : Two 
 
-record TwoCat  {c₁ c₂ ℓ : Level} (I : Category c₁ c₂ ℓ) 
-      (two : Two {c₁}) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
-   field
-       obj  : Two {c₁}  → Obj I
-       obj← : Obj I → Two  
-       map  : Two {c₁} → Hom I (obj t0) (obj t1) 
-       map← : Hom I (obj t0) (obj t1) → Two {c₁}  
-       unique-obj  :  ∀{two : Two } → obj← ( obj two ) ≡ two
-       unique-obj1 :  ∀{i : Obj I } → obj ( obj← i ) ≡ i
-       unique-map  :  ∀{two : Two } → map← ( map two ) ≡ two
-       unique-map1 :  ∀{f : Hom I (obj t0) (obj t1) } → map ( map← f ) ≡ f
+
+infixr 40 _::_
+data  List {a} (A : Set a)  : Set a where
+   [] : List A
+   _::_ : A -> List A -> List A
+
+-- record TwoCat {ℓ} (S : Sets {ℓ}) : Set ℓ where
+--    field
+--         twoSet : TwoSet S
+--         hom : TwoSet S → TwoSet S → Set _
+
+
+twocat : {c₁ c₂ ℓ : Level} → (id-0 id-1 f g : Set  c₂) → Category c₁ _ ℓ
+twocat {c₁} {c₂} {ℓ} id-0 id-1 f g = record {
+    Obj  = Two {c₁} ;
+    Hom = λ a b →  List (Set  c₂) ;
+    _o_ =  {!!} ;
+    _≈_ = {!!} ;
+    Id  = {!!} ;
+    isCategory  = record {
+            isEquivalence = {!!} ;
+            identityL  = {!!} ;
+            identityR  = {!!} ;
+            o-resp-≈  = {!!} ;
+            associative  = {!!}
+       } 
+   } where
+        hom : Two {c₁} → Two {c₁} → List (Set  c₂)
+        hom t0 t0 =  id-0 :: []
+        hom t0 t1 =  f :: g :: []
+        hom t1 t0 =  []
+        hom t1 t1 =  id-1 :: []
 
 open Limit
-open TwoCat
-
-record two-Γ  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) 
-       (a b : Obj A)  (f g : Hom A a b )
-       (two : Two) (twocat : TwoCat I two ) (Γ : Functor I A) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ))  where
-    field
-       a0  :  FObj Γ (obj twocat t0 ) ≡ a 
-       b0  :  FObj Γ (obj twocat t1 ) ≡ b 
-       f0  :  A [ FMap Γ (map twocat t0 ) ≈ f ]
-       g0  :  A [ FMap Γ (map twocat t0 ) ≈ g ]
 
 lim-to-equ : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ)
-      (two : Two  ) 
-      (twocat : TwoCat I two) 
-      (Γ : Functor I A)
+      (two : {!!}  ) 
       (lim : ( Γ : Functor I A ) → { a0 : Obj A } { u : NTrans I A ( K A I a0 ) Γ } → Limit A I Γ a0 u ) -- completeness
         →  {a b c : Obj A} (f g : Hom A a b)  → (e : Hom A c a ) → (fe=ge : A [ A [ f o e ] ≈ A [ g o e ] ] ) → Equalizer A e f g
-lim-to-equ {c₁} A I two twocat Γ lim {a} {b} {c} f g e fe=ge = record {
+lim-to-equ {c₁} A I two lim {a} {b} {c} f g e fe=ge = record {
         fe=ge =  fe=ge
         ; k = λ {d} h fh=gh → k {d} h fh=gh
         ; ek=h = λ {d} {h} {fh=gh} → {!!}
         ; uniqueness = λ {d} {h} {fh=gh} {k'} → {!!}
      } where
+         Γobj :  Two {c₁} → Obj A
+         Γobj t0 = a
+         Γobj t1 = b
+         Γmap :  Two {c₁} → Hom A a b
+         Γmap t0 = f
+         Γmap t1 = g
+         Γ : Functor I A
+         Γ = record {
+            FObj  = λ x → Γobj {!!} ;
+            FMap  = λ f → {!!} ;
+            isFunctor = record {
+                     ≈-cong  = {!!} ; 
+                    identity = {!!} ;
+                    distr = {!!}
+            }
+          }
          nat : (d : Obj A) → NTrans I A (K A I d) Γ
          nat d = record {
             TMap = λ x → {!!} ;