# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1458021148 -32400
# Node ID 2ee1496b31d7d10cbd0b714fd8c1c0f81ca7cfad
# Parent  1301270b89428c98139728fb9a1206e33fd581d1
fix

diff -r 1301270b8942 -r 2ee1496b31d7 limit-to.agda
--- a/limit-to.agda	Tue Mar 15 11:45:43 2016 +0900
+++ b/limit-to.agda	Tue Mar 15 14:52:28 2016 +0900
@@ -35,16 +35,15 @@
 record RawHom {c₁ ℓ : Level}  (a : TwoObject {c₁}  ) (b : TwoObject {c₁}  ) : Set  (c₁  ⊔ ℓ) where
    field
        RawMap    : Arrow  {ℓ }
-       isNull    : TwoObject  {c₁}
 
 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 ; isNull = t0  } 
-arrow2hom t1 t1 id-t1 =  record { RawMap = id-t1 ; isNull = t0  } 
-arrow2hom t0 t1 arrow-f =  record { RawMap = arrow-f ; isNull = t0 } 
-arrow2hom t0 t1 arrow-g =  record { RawMap = arrow-g ; isNull = t0  } 
-arrow2hom _ _ f  =  record { RawMap = f ; isNull = t1  } 
+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 } 
 
 record Two-Hom { c₁  ℓ : Level }   (a : TwoObject { c₁}  ) (b : TwoObject  { c₁} ) : Set   (c₁  ⊔ ℓ)  where
    field
@@ -54,13 +53,13 @@
    Map = RawMap hom
 
 Two-id :  {c₁ ℓ : Level } -> (a : TwoObject {c₁} ) ->   Two-Hom {c₁} { ℓ} a a 
-Two-id t0  = record { hom = record { isNull = t0 ;RawMap = id-t0  } ;   arrow-iso = refl }
-Two-id t1  = record { hom = record { isNull = t0 ;RawMap = id-t1  } ;   arrow-iso = refl }
+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 ; isNull = t1 }
+      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
@@ -74,20 +73,32 @@
 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 = 
-           record { RawMap =     arrow ; isNull = nul } ;  
-                    arrow-iso =  arrow-iso a c ( arrow ) nul }
+_×_   { c₁} {ℓ} {a} {b} {c} f g  = record { hom =  arrow ;
+                    arrow-iso =  arrow-iso a c  (RawMap arrow  ) }
    where
-      arrow  =   twocomp  {ℓ} (Two-Hom.Map f) (Two-Hom.Map g) 
-      nul  =   isNull ( arrow2hom a b arrow  )
-      arrow-iso : {c₁ ℓ : Level } -> ( a b : TwoObject  {c₁} ) -> (f : Arrow { ℓ} ) -> ( n : TwoObject {c₁} ) -> 
-             arrow2hom {c₁} {ℓ } a b f  ≡ record { RawMap = f ; isNull = n }
-      arrow-iso t0 t0 id-t0  t0 = refl
-      arrow-iso t1 t1 id-t1  t0 = refl
-      arrow-iso t0 t1 arrow-f  t0 = refl
-      arrow-iso t0 t1 arrow-g  t0 = refl
-      arrow-iso _ _ _  t0 = {!!}
-      arrow-iso _ _ _  t1 = ?
+      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
 
 open Two-Hom
 
@@ -110,7 +121,17 @@
         open  import  Relation.Binary.PropositionalEquality
         ≡-cong = Relation.Binary.PropositionalEquality.cong 
         identityL : {A B : TwoObject} {f : Two-Hom A B} →  Map ( Two-id B × f ) ≡ Map f
-        identityL {a} {b} {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
+              begin
+                 {!!}
+              ≡⟨ {!!} ⟩
+                 id-t0
+              ∎
+        identityL {_} {_} {f}  | _ =  {!!}
+
         identityR : {A B : TwoObject} {f : Two-Hom A B} →  Map ( f × Two-id A  ) ≡ Map f
         identityR {a} {b} {f} = {!!}
         o-resp-≈ : {A B C : TwoObject} {f g :  Two-Hom A B} {h i : Two-Hom B C} →
@@ -118,13 +139,9 @@
         o-resp-≈  {a} {b} {c} {f} {g} {h} {i}  f≡g h≡i  = let open ≡-Reasoning in
               begin
                  Map (h × f)
-              ≡⟨⟩
-                 twocomp (Map h) (Map f)
-              ≡⟨ ≡-cong (\x -> twocomp (Map h) x )  f≡g  ⟩
-                 twocomp (Map h) (Map g)
-              ≡⟨ ≡-cong (\x -> twocomp x (Map g) )  h≡i  ⟩
-                 twocomp (Map i) (Map g)
-              ≡⟨⟩
+              ≡⟨  ≡-cong (\x ->  RawMap ( arrow2hom a c ( twocomp (Map h) x )) )  f≡g  ⟩
+                 Map (h × g)
+              ≡⟨  ≡-cong (\x ->  RawMap ( arrow2hom a c ( 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 )