--- a/limit-to.agda	Sat Mar 26 17:18:49 2016 +0900
+++ b/limit-to.agda	Sat Mar 26 20:00:34 2016 +0900
@@ -333,50 +333,9 @@
 --        →  ( 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}  | _ | _ = {!!}
+--   this one does not work on fmap ( g o f )  ≈  ( fmap g o fmap f )
+--      because  g o f can be arrow-f when g is arrow-g
+--      ideneity and ≈-cong are easy
 
 
 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