--- a/limit-to.agda	Sat Mar 26 15:51:30 2016 +0900
+++ b/limit-to.agda	Sat Mar 26 17:18:49 2016 +0900
@@ -328,6 +328,56 @@
           ≈-cong {a} {b} {f} {g} nothing | nothing  | nothing = let open ≈-Reasoning (A) in  refl-hom
           ≈-cong {a} {b} {f} {g} (just eq) | just _ | just _ = eq
 
+-- indexFunctor' :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (none : Nil A) ( a b : Obj A) ( f g : Hom A a b ) 
+--        →  ( obj→ : Obj A -> TwoObject  {c₁}  )
+--        →  ( hom→ : { a b : Obj A } -> Hom A a b -> Arrow t0 t0 (obj→ a) (obj→ b)   )
+--        →  ( { x y : Obj A } { h i : Hom A x y } -> A [ h  ≈ i ]  →  hom→  h ≡ hom→  i  )
+--        →  Functor A A
+-- indexFunctor'  {c₁} {c₂} {ℓ} A none a b f g obj→  hom→  hom-≡ =  record {
+--          FObj = λ a → fobj' a
+--        ; FMap = λ {a} {b} f → fmap' {a} {b} f
+--        ; isFunctor = record {
+--              identity = λ{x} → identity2 {x}
+--              ; distr = λ {a} {b} {c} {f} {g}   →  distr2 {a} {b} {c} {f} {g}
+--              ; ≈-cong = λ {a} {b} {c} {f}   →  ≈-cong2  {a} {b} {c} {f}
+--        }
+--       } where
+--           open  ≈-Reasoning A
+--           fobj' :  Obj A → Obj A
+--           fobj' x with obj→ x
+--           fobj' x | t0 =  a
+--           fobj' x | t1 =  b
+--           fmap2 : TwoObject  {c₁}   → Hom A a b
+--           fmap2 t0 = f
+--           fmap2 t1 = g
+--           fmap' :  {x y : Obj A } →  Hom A x y → Hom A (fobj' x) (fobj' y )
+--           fmap' {x} {y} h with  obj→ x | obj→ y | hom→ h
+--           fmap' {x} {y} h | t0 | t0 | id-t0 = id1 A a
+--           fmap' {x} {y} h | t1 | t1 | id-t0 = id1 A b
+--           fmap' {x} {y} h | t0 | t1 | arrow-f = f
+--           fmap' {x} {y} h | t0 | t1 | arrow-f = g
+--           fmap' {x} {y} h | _ | _ | _ = nil none
+--           identity2 :  {x : Obj A} → A [ fmap' ( id1 A x ) ≈  id1 A (fobj' x) ]
+--           identity2 {x} with obj→ x
+--           identity2 {x} | t0  =  refl-hom
+--           identity2 {x} | t1  =  refl-hom
+--           ≈-cong2 :   {x : Obj A} {y : Obj A} {f1 g1 : Hom A x y}  → A [ f1 ≈ g1 ]  → A [ fmap' f1 ≈ fmap' g1 ]
+--           ≈-cong2   {x} {y} {f1} {g1} f≈g with obj→ x | obj→ y | hom→ f1 
+--           ≈-cong2   {x} {y} {f1} {g1} f≈g | t0 | t0 | _  =   refl-hom
+--           ≈-cong2   {x} {y} {f1} {g1} f≈g | t1 | t1 | _  =   refl-hom
+--           ≈-cong2   {x} {y} {f1} {g1} f≈g | t0 | t1 | t0  =   begin
+--                     f
+--                 ≈⟨⟩
+--                     fmap2  t0 
+--                 ≈⟨  ≡-cong (\x -> fmap2 x ) ( hom-≡  f≈g)   ⟩
+--                     fmap2 ( hom→ g1 )
+--                 ∎
+--           ≈-cong2   {x} {y} {f1} {g1} f≈g | _  |  _ | _  = {!!}
+--           distr2 : {a₁ : Obj A} {b₁ : Obj A} {c : Obj A} {f₁ : Hom A a₁ b₁} {g₁ : Hom A b₁ c} →
+--                A [ fmap' (A [ g₁ o f₁ ])  ≈  A [ fmap' g₁ o fmap' f₁ ] ]
+--           distr2 {a1} {b1} {c1} {f1} {g1}   with hom→ g1 | hom→ f1
+--           distr2 {a1} {b1} {c1} {f1} {g1}  | _ | _ = {!!}
+
 
 indexFunctor :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (none : Nil A) ( a b : Obj A) ( f g : Hom A a b ) →  Functor (TwoCat {c₁} {c₂} {c₂} ) A
 indexFunctor  {c₁} {c₂} {ℓ} A none a b f g = record {
@@ -421,10 +471,10 @@
 ---     | /             |
 ---     |/              | Γ
 ---     d _             |
----      |λ             |
----        λ K          af
----         λ        -----→
----          λ     t0        t1
+---      |\             |
+---        \ K          af
+---         \        -----→
+---          \     t0        t1
 ---                  -----→
 ---                     ag
 ---