# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1458717923 -32400
# Node ID e08af559efb9673585a963ed328290dc8954eb5f
# Parent  f04b2fb914328c5c2d9213d830d530822595f2a3
reverse arrow must be there...

diff -r f04b2fb91432 -r e08af559efb9 limit-to.agda
--- a/limit-to.agda	Wed Mar 23 15:45:05 2016 +0900
+++ b/limit-to.agda	Wed Mar 23 16:25:23 2016 +0900
@@ -29,8 +29,9 @@
 
 record TwoHom {c₁ c₂ : Level}  (a : TwoObject {c₁}  ) (b : TwoObject {c₁}  ) : Set   c₂ where
    field
-       Map    : TwoObject  {c₂ }
+       hom    : TwoObject  {c₂ }
 
+open TwoHom
 
 -- arrow composition
 
@@ -99,20 +100,31 @@
        ( f × (g × h)) == ((f × g) × h )
 assoc-× {_} {_} {_} {_} {_} {_} {nothing} {_} {_} = nothing
 assoc-× {_} {_} {_} {_} {_} {_} {just _} {nothing} {_} = nothing
-assoc-× {c₁} {c₂} {a} {b} {c} {d} {just f} {just g} {nothing} =  let open ==-Reasoning {c₁} {c₂} in 
-    begin
-        ?
-    ==⟨ ? ⟩ 
-         ?
-    ∎
-assoc-× {_} {_} {_} {_} {_} {_} {just _} {just _} {just _} = ?
+assoc-× {c₁} {c₂} {a} {b} {c} {d} {just f} {just g} {nothing} with  (just f × just g)
+assoc-× {c₁} {c₂} {a} {b} {c} {d} {just f} {just g} {nothing} | nothing =   ==refl
+assoc-× {c₁} {c₂} {a} {b} {c} {d} {just f} {just g} {nothing} | just h =  ==refl
+assoc-× {_} {_} {t0} {t0} {t0} {t0} {just _} {just _} {just _} = ==refl
+assoc-× {_} {_} {t0} {t0} {t0} {t1} {just _} {just _} {just _} = ==refl
+assoc-× {_} {_} {t0} {t0} {t1} {t0} {just _} {just _} {just _} = ==refl
+assoc-× {_} {_} {t0} {t0} {t1} {t1} {just _} {just _} {just _} = ==refl
+assoc-× {_} {_} {t0} {t1} {t0} {t0} {just _} {just _} {just _} = ==refl
+assoc-× {_} {_} {t0} {t1} {t0} {t1} {just _} {just _} {just _} = ==refl
+assoc-× {_} {_} {t0} {t1} {t1} {t0} {just _} {just _} {just _} = ==refl
+assoc-× {_} {_} {t0} {t1} {t1} {t1} {just _} {just _} {just _} = ==refl
+assoc-× {_} {_} {t1} {t0} {t0} {t0} {just _} {just _} {just _} = ==refl
+assoc-× {_} {_} {t1} {t0} {t0} {t1} {just _} {just _} {just _} = ==refl
+assoc-× {_} {_} {t1} {t0} {t1} {t0} {just _} {just _} {just _} = ==refl
+assoc-× {_} {_} {t1} {t0} {t1} {t1} {just _} {just _} {just _} = ==refl
+assoc-× {_} {_} {t1} {t1} {t0} {t0} {just _} {just _} {just _} = ==refl
+assoc-× {_} {_} {t1} {t1} {t0} {t1} {just _} {just _} {just _} = ==refl
+assoc-× {_} {_} {t1} {t1} {t1} {t0} {just _} {just _} {just _} = ==refl
+assoc-× {_} {_} {t1} {t1} {t1} {t1} {just _} {just _} {just _} = ==refl
 
 
 
-
-TwoId :  {c₁  c₂ : Level } {a : TwoObject  {c₁} } ->  Maybe (TwoHom {c₁}  {c₂ } a a )
-TwoId {_} {_} {_} = just ?
-
+TwoId :  {c₁  c₂ : Level } (a : TwoObject  {c₁} ) ->  Maybe (TwoHom {c₁}  {c₂ } a a )
+TwoId {_} {_} t0 = just  record { hom = t0 } 
+TwoId {_} {_} t1 = just  record { hom = t1 } 
 
 open import maybeCat  
 
@@ -124,15 +136,34 @@
     Hom = λ a b →    Maybe ( TwoHom {c₁}  {c₂ } a b ) ;
     _o_ =  \{a} {b} {c} x y -> _×_ {c₁ } { c₂} {a} {b} {c} x y ;
     _≈_ =    Eq  _≡_   ;
-    Id  =  \{a} -> TwoId {c₁ } { c₂} {a} ;
+    Id  =  \{a} -> TwoId {c₁ } { c₂} a ;
     isCategory  = record {
             isEquivalence =  record {refl = ==refl ; trans = ==trans ; sym = ==sym } ;
-            identityL  = {!!} ;
-            identityR  = {!!} ;
-            o-resp-≈  =  {!!} ;
-            associative  = assoc-×
+            identityL  = \{a b f} -> identityL {c₁}  {c₂ } {a} {b} {f} ;
+            identityR  = \{a b f} -> identityR {c₁}  {c₂ } {a} {b} {f} ;
+            o-resp-≈  = \{a b c f g h i} ->  o-resp-≈  {c₁}  {c₂ } {a} {b} {c} {f} {g} {h} {i} ;
+            associative  = \{a b c d f g h } -> assoc-×   {c₁}  {c₂} {a} {b} {c} {d} {f} {g} {h}
        } 
-   } 
+   }  where
+        identityL :  {c₁  c₂ : Level } {A B : TwoObject {c₁}} {f : Maybe ( TwoHom {c₁}  {c₂ } A B) } →  ((TwoId B)  × f)  == f
+        identityL {_} {_}  {_} {_} {nothing}  = {!!}
+        identityL {_} {_}  {t0} {t0} {just f}  = ==refl
+        identityL {_} {_}  {t0} {t1} {just f}  = ==refl
+        identityL {_} {_}  {t1} {t1} {just f}  = ==refl
+        identityL   {c₁}  {c₂}  {t1} {t0} {just f}  =  let open ==-Reasoning  {c₁}  {c₂} in
+                begin 
+                  (TwoId t0 × just f)
+                ==⟨⟩
+                   nothing
+                ==⟨ {!!} ⟩
+                   just f
+                ∎ 
+        identityR :  {c₁  c₂ : Level } {A B : TwoObject {c₁}} {f : Maybe ( TwoHom {c₁}  {c₂ } A B) } →   ( f × TwoId A )  == f
+        identityR {_} {_} {a} {b} {f}  = {!!}
+        o-resp-≈ :  {c₁  c₂ : Level } {A B C : TwoObject  {c₁} } {f g :  Maybe ( TwoHom {c₁}  {c₂ } A B)} {h i : Maybe ( TwoHom B C)} →
+            f == g → h == i → ( h × f ) == ( i × g )
+        o-resp-≈  {_} {_} {a} {b} {c} {f} {g} {h} {i}  f≡g h≡i  = {!!}
+
 
 indexFunctor :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( a b : Obj (MaybeCat A )) ( f g : Hom A a b ) ->  Functor (TwoCat {c₁} {c₂} {c₂} ) (MaybeCat A )
 indexFunctor  {c₁} {c₂} {ℓ} A  a b f g = record {
@@ -151,7 +182,7 @@
           fobj t0 = a
           fobj t1 = b
           fmap :  {x y : Obj I } ->  Maybe (TwoHom {c₁}  {c₂} x y  ) -> Hom MA (fobj x) (fobj y)
-          fmap  = ?
+          fmap  = {!!}
           open ≈-Reasoning (A) 
           identity :  {x : Obj I} → {!!}
           identity {t0}  =  {!!}