--- a/limit-to.agda	Tue Mar 15 14:52:28 2016 +0900
+++ b/limit-to.agda	Tue Mar 15 16:11:37 2016 +0900
@@ -27,10 +27,11 @@
 
 data Arrow {ℓ : Level }  : Set ℓ where
    id-t0 : Arrow  
-   id-t1 : Arrow  
    arrow-f :  Arrow
    arrow-g :  Arrow
-   nil :  Arrow -- inconsitent hom
+   reverse-f :  Arrow
+   reverse-g :  Arrow
+   nil :  Arrow
 
 record RawHom {c₁ ℓ : Level}  (a : TwoObject {c₁}  ) (b : TwoObject {c₁}  ) : Set  (c₁  ⊔ ℓ) where
    field
@@ -38,67 +39,48 @@
 
 open RawHom
 
-arrow2hom :  {c₁ ℓ : Level}  -> (a : TwoObject {c₁}  ) (b : TwoObject {c₁}  ) -> Arrow  {ℓ } -> RawHom  { c₁}  {ℓ } a b
-arrow2hom t0 t0 id-t0 =  record { RawMap = id-t0 } 
-arrow2hom t1 t1 id-t1 =  record { RawMap = id-t1 } 
-arrow2hom t0 t1 arrow-f =  record { RawMap = arrow-f } 
-arrow2hom t0 t1 arrow-g =  record { RawMap = arrow-g } 
-arrow2hom _ _ f  =  record { RawMap = f } 
+arrow2hom :  {c₁ ℓ : Level}  -> {a : TwoObject {c₁}  } {b : TwoObject {c₁}  } -> Arrow  {ℓ } -> RawHom  { c₁}  {ℓ } a b
+arrow2hom id-t0 =  record { RawMap = id-t0 } 
+arrow2hom arrow-f =  record { RawMap = arrow-f } 
+arrow2hom arrow-g =  record { RawMap = arrow-g } 
+arrow2hom reverse-f =  record { RawMap = reverse-f } 
+arrow2hom reverse-g =  record { RawMap = reverse-g } 
+arrow2hom nil =  record { RawMap = nil } 
 
 record Two-Hom { c₁  ℓ : Level }   (a : TwoObject { c₁}  ) (b : TwoObject  { c₁} ) : Set   (c₁  ⊔ ℓ)  where
    field
       hom : RawHom { c₁}  {ℓ } a b
-      arrow-iso : arrow2hom a b ( RawMap hom ) ≡ hom
+      arrow-iso : arrow2hom ( RawMap hom )  ≡ hom
    Map : Arrow
    Map = RawMap hom
 
 Two-id :  {c₁ ℓ : Level } -> (a : TwoObject {c₁} ) ->   Two-Hom {c₁} { ℓ} a a 
-Two-id t0  = record { hom = record { RawMap = id-t0  } ;   arrow-iso = refl }
-Two-id t1  = record { hom = record { RawMap = id-t1  } ;   arrow-iso = refl }
-
-Two-nothing : {c₁ ℓ : Level } -> ( a b : TwoObject  {c₁} ) -> Two-Hom  {c₁} { ℓ} a b
-Two-nothing a b  = record { hom = record { RawMap = nil } ; arrow-iso = arrow-iso  a b }
-   where
-      arrow-iso : {c₁ ℓ : Level } -> ( a b : TwoObject  {c₁} ) -> arrow2hom {c₁} {ℓ } a b nil ≡ record { RawMap = nil }
-      arrow-iso  t0 t0 =  refl
-      arrow-iso  t0 t1 =  refl
-      arrow-iso  t1 t0 =  refl
-      arrow-iso  t1 t1 =  refl
+Two-id _  = record { hom = record { RawMap = id-t0 } ;   arrow-iso = refl }
 
 -- arrow composition
 
 twocomp :  {ℓ : Level } -> Arrow {ℓ } -> Arrow {ℓ } -> Arrow {ℓ } 
 twocomp id-t0  f  = f
 twocomp f id-t0 = f
+twocomp arrow-f reverse-f = id-t0
+twocomp arrow-g reverse-g = id-t0
+twocomp reverse-f arrow-f = id-t0
+twocomp reverse-g arrow-g = id-t0
 twocomp _ _ = nil
 
 _×_ :  { c₁  ℓ : Level }  -> {A B C : TwoObject { c₁} } →  Two-Hom { c₁}  {ℓ}  B C →  Two-Hom { c₁}  {ℓ}  A B  →  Two-Hom { c₁}  {ℓ}  A C 
 _×_   { c₁} {ℓ} {a} {b} {c} f g  = record { hom =  arrow ;
-                    arrow-iso =  arrow-iso a c  (RawMap arrow  ) }
+                    arrow-iso =  arrow-iso   (RawMap arrow  ) }
    where
-      arrow  =   arrow2hom a c ( twocomp  {ℓ} (Two-Hom.Map f) (Two-Hom.Map g)  )
-      arrow-iso : {c₁ ℓ : Level } -> ( a b : TwoObject  {c₁} ) -> (f : Arrow { ℓ} ) -> 
-             arrow2hom {c₁} {ℓ } a b f  ≡ record { RawMap = f }
-      arrow-iso t0 t0 id-t0  = refl
-      arrow-iso t1 t1 id-t1  = refl
-      arrow-iso t0 t1 arrow-f  = refl
-      arrow-iso t0 t1 arrow-g  = refl
-      arrow-iso t0 t0 nil  = refl
-      arrow-iso t0 t1 nil  = refl
-      arrow-iso t1 t0 nil  = refl
-      arrow-iso t1 t1 nil  = refl
-      arrow-iso t0 t1 id-t0  = refl
-      arrow-iso t1 t0 id-t0  = refl
-      arrow-iso t1 t1 id-t0  = refl
-      arrow-iso t0 t1 id-t1  = refl
-      arrow-iso t1 t0 id-t1  = refl
-      arrow-iso t0 t0 id-t1  = refl
-      arrow-iso t1 t0 arrow-f  = refl
-      arrow-iso t1 t1 arrow-f  = refl
-      arrow-iso t0 t0 arrow-f  = refl
-      arrow-iso t1 t0 arrow-g  = refl
-      arrow-iso t1 t1 arrow-g  = refl
-      arrow-iso t0 t0 arrow-g  = refl
+      arrow  =   arrow2hom {c₁ } {ℓ } {a} {c} ( twocomp  {ℓ} (Two-Hom.Map f) (Two-Hom.Map g)  ) 
+      arrow-iso : (f : Arrow { ℓ} ) -> 
+             arrow2hom {c₁} {ℓ } {a} {c} f ≡ record { RawMap = f }
+      arrow-iso   id-t0 = refl
+      arrow-iso  arrow-f = refl
+      arrow-iso  arrow-g = refl
+      arrow-iso  reverse-f = refl
+      arrow-iso  reverse-g = refl
+      arrow-iso  nil = refl
 
 open Two-Hom
 
@@ -123,10 +105,14 @@
         identityL : {A B : TwoObject} {f : Two-Hom A B} →  Map ( Two-id B × f ) ≡ Map f
         identityL {a} {b} {f} with Map f
         identityL {t0} {t0} {f}  | id-t0 =  refl
-        identityL {t0} {t0} {f}  | id-t1 =  refl
-        identityL {_} {t0} {f}  | id-t0 =  let open ≡-Reasoning in
+        identityL {t1} {t0} {f}  | id-t0 =  refl
+        identityL {t0} {t0} {f}  | nil =  refl
+        identityL {t0} {t1} {f}  | nil =  refl
+        identityL {t1} {t0} {f}  | nil =  refl
+        identityL {t1} {t1} {f}  | nil =  refl
+        identityL {a} {t1} {f}  | id-t0 =  let open ≡-Reasoning in
               begin
-                 {!!}
+                  {!!}
               ≡⟨ {!!} ⟩
                  id-t0
               ∎
@@ -139,9 +125,9 @@
         o-resp-≈  {a} {b} {c} {f} {g} {h} {i}  f≡g h≡i  = let open ≡-Reasoning in
               begin
                  Map (h × f)
-              ≡⟨  ≡-cong (\x ->  RawMap ( arrow2hom a c ( twocomp (Map h) x )) )  f≡g  ⟩
+              ≡⟨  ≡-cong (\x ->  RawMap ( arrow2hom  ( twocomp (Map h) x ) ) )  f≡g  ⟩
                  Map (h × g)
-              ≡⟨  ≡-cong (\x ->  RawMap ( arrow2hom a c ( twocomp x (Map g) )) )  h≡i  ⟩
+              ≡⟨  ≡-cong (\x ->  RawMap ( arrow2hom  ( twocomp x (Map g) ) ) )  h≡i  ⟩
                  Map (i × g)
               ∎
         associative : {A B C D : TwoObject} {f : Two-Hom C D} {g : Two-Hom B C} {h : Two-Hom A B} → Map ( f × (g × h) ) ≡ Map ( (f × g) × h )