--- a/limit-to.agda	Sun Mar 06 17:33:56 2016 +0900
+++ b/limit-to.agda	Thu Mar 10 19:56:12 2016 +0900
@@ -41,11 +41,15 @@
          obj-rev : {a : TwoObject } -> obj→ ( obj← a) ≡ a
          hom→ : { x y : Obj I  } -> Hom I x y -> TwoObject
          hom← : TwoObject  -> Hom I ( obj← t0 ) ( obj← t1)
+         cong-hom→ : { x y : Obj I  } -> {f g : Hom I x y } ->  I [ f ≈  g ] ->  hom→ f  ≡   hom→ g
          hom-iso : {a :  Hom I ( obj← t0 ) ( obj← t1)} -> hom← ( hom→ a) ≡ a
          hom-rev : {a : TwoObject } -> hom→ ( hom← a) ≡ a
          f-rev : Hom A b a   
          feq : A [ A [ f-rev o  f ] ≈  id1 A a ]
          geq : A [ A [ f-rev o  g ] ≈  id1 A a ]
+         feq' : A [ A [ f o  f-rev ] ≈  id1 A b ]
+         geq' : A [ A [ g o  f-rev ] ≈  id1 A b ]
+         I-id : { d : Obj I } -> ( i : Hom I d d ) -> I [ i  ≈  id1 I d ]
     fobj : Obj I -> Obj A
     fobj  x with obj→ x 
     fobj  x | t0 = a
@@ -53,6 +57,14 @@
     fmap' :   TwoObject -> Hom A a b
     fmap' t0 = f
     fmap' t1 = g
+    two-lemma-1 : {x y : Obj I } -> (i : Hom I x y ) ->  A [ A [ f-rev o fmap' ( hom→  i ) ]  ≈  id1 A a  ] 
+    two-lemma-1 i with hom→ i
+    ... | t0 =  feq
+    ... | t1 =  geq
+    two-lemma-2 : {x y : Obj I } -> (i : Hom I x y ) ->  A [ A [ fmap' ( hom→  i ) o f-rev ]  ≈  id1 A b  ] 
+    two-lemma-2 i with hom→ i
+    ... | t0 =  feq'
+    ... | t1 =  geq'
 
 open TwoCat
 
@@ -80,24 +92,36 @@
           ... | t1 = let open ≈-Reasoning (A) in refl-hom
           distr : {a₁ : Obj I} {b₁ : Obj I} {c : Obj I} {f₁ : Hom I a₁ b₁} {g₁ : Hom I b₁ c} → A [ fmap (I [ g₁ o f₁ ]) ≈ A [ fmap g₁ o fmap f₁ ] ]
           distr {a₁} {b₁} {c} {f₁} {g₁}  with obj→  two  c   | obj→  two  b₁  | obj→  two  a₁
-          ... | t0 | t0 | t0 = let open ≈-Reasoning (A) in
+          ... | t0 | t0 | t0 = let open ≈-Reasoning (A) in sym idL
+          ... | t0 | t0 | t1 = let open ≈-Reasoning (A) in sym idL
+          ... | t0 | t1 | t0 = let open ≈-Reasoning (A) in
               begin
-                 id1 A a
-              ≈↑⟨ idL ⟩
-                 id1 A a  o id1 A a
+                id1 A a
+              ≈↑⟨ two-lemma-1 two  f₁  ⟩
+                f-rev two  o fmap' two ( hom→  two  f₁ )
               ∎
-          ... | t0 | t0 | t1 = let open ≈-Reasoning (A) in 
+          ... | t0 | t1 | t1 = let open ≈-Reasoning (A) in 
               begin
-                  ?
-              ≈⟨ {!!} ⟩
-                 {!!}
+                f-rev two
+              ≈↑⟨ idR ⟩
+                 f-rev two o id1 A b
               ∎
-          ... | t0 | t1 | t0 = {!!} 
-          ... | t0 | t1 | t1 = {!!} 
-          ... | t1 | t0 | t0 = {!!}
-          ... | t1 | t0 | t1 = {!!}
-          ... | t1 | t1 | t0 = {!!}
-          ... | t1 | t1 | t1 = let open ≈-Reasoning (A) in {!!}
+          ... | t1 | t0 | t0 = let open ≈-Reasoning (A) in  
+              begin
+                fmap' two ( hom→  two ( I [ g₁ o f₁ ] ))
+              ≈↑⟨  ≡-cong  (cong-hom→ two  ( {!!} ) ) (\x -> fmap' two x )  ⟩
+                fmap' two ( hom→  two  g₁ )   
+              ≈↑⟨ idR ⟩
+                fmap' two ( hom→  two  g₁ )   o id1 A a
+              ∎
+          ... | t1 | t0 | t1 = let open ≈-Reasoning (A) in 
+              begin
+                id1 A b
+              ≈↑⟨ two-lemma-2 two  g₁  ⟩
+                fmap' two ( hom→  two  g₁ ) o f-rev two
+              ∎
+          ... | t1 | t1 | t0 = let open ≈-Reasoning (A) in {!!}
+          ... | t1 | t1 | t1 = let open ≈-Reasoning (A) in sym idR
           ≈-cong :   {a : Obj I} {b : Obj I} {f g : Hom I a b}  → I [ f ≈ g ] → A [ fmap f ≈ fmap g ]
           ≈-cong {a} {b} {f} {g}  f≈g = let open ≈-Reasoning (A) in {!!}