--- a/limit-to.agda	Wed Mar 16 15:44:46 2016 +0900
+++ b/limit-to.agda	Wed Mar 16 17:43:31 2016 +0900
@@ -168,13 +168,13 @@
 
 
 indexFunctor :  {c₁ c₂ ℓ : Level}  (A : Category c₁ c₂ ℓ) 
-        ( a b : Obj A ) ( f g : Hom A a b )   ( f' : Hom A b a )  
+        ( a b : Obj A ) ( f g h : Hom A a b )   ( h' : Hom A b a )  
              ( f-iso :  A [ A [ f   o f' ]  ≈ id1 A b ])  
              ( f'-iso : A [ A [ f'  o f  ]  ≈ id1 A a ])  
              ( g-iso :  A [ A [ g   o f' ]  ≈ id1 A b ])  
              ( g'-iso : A [ A [ f'  o g  ]  ≈ id1 A a ])  
              ->  Functor (TwoCat {c₁} {c₂} {ℓ} ) A
-indexFunctor  {c₁} {c₂} {ℓ} A a b f g f'  f-iso f'-iso g-iso g'-iso = record {
+indexFunctor  {c₁} {c₂} {ℓ} A a b f g h h'  f-iso f'-iso g-iso g'-iso = record {
          FObj = λ a → fobj a
        ; FMap = λ f → fmap f
        ; isFunctor = record {
@@ -193,9 +193,13 @@
           fmap1 {t0} {t0}   id-t0  = id1 A a
           fmap1 {t1} {t1}   id-t0  = id1 A b
           fmap1 {t0} {t0}   _ = id1 A a
-          fmap1 {t0} {t1}   _ = f
-          fmap1 {t1} {t0}   _ = f'
           fmap1 {t1} {t1}   _ = id1 A b
+          fmap1 {t0} {t1}   nil = h
+          fmap1 {t0} {t1}   id-t0 = h
+          fmap1 {t1} {t0}   nil = h'
+          fmap1 {t1} {t0}   id-t0 = h'
+          fmap1 {t1} {t0}   arrow-f = h'
+          fmap1 {t1} {t0}   arrow-g = h'
           fmap :  {x y : Obj I } -> Hom I x y -> Hom A (fobj x) (fobj y)
           fmap {x} {y} f  = fmap1 {x} {y} ( Map f)
           open ≈-Reasoning (A) 

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/maybeCat.agda	Wed Mar 16 17:43:31 2016 +0900
@@ -0,0 +1,61 @@
+open import Category -- https://github.com/konn/category-agda                                                                                     
+open import Level
+
+module maybeCat { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } where
+
+open import cat-utility
+open import HomReasoning
+open import Relation.Binary 
+open import Data.Maybe
+
+open Functor
+
+
+record MaybeHom { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  (a : Obj A ) (b : Obj A ) : Set  (ℓ ⊔ c₂)   where
+   field
+      hom : Maybe ( Hom A a b )
+
+open MaybeHom
+
+_×_ :    {a b c : Obj A } → MaybeHom A b c  →  MaybeHom A a b  →  MaybeHom A  a c 
+_×_   {a} {b} {c} f g with hom f | hom g
+_×_   {a} {b} {c} f g | nothing  | _  = record { hom =  nothing }
+_×_   {a} {b} {c} f g | _ | nothing   = record { hom =  nothing }
+_×_   {a} {b} {c} _ _ | (just f) |  (just g)  = record { hom =  just ( A [ f o  g ]  ) }
+
+MaybeHomId  : (a  : Obj A ) -> MaybeHom A a a
+MaybeHomId  a  = record { hom = just ( id1 A a)  }
+
+_==_ :  {a b : Obj A } ->  Rel (Maybe (Hom A a b)) (c₂ ⊔ ℓ) 
+_==_   {a} {b}  =   Eq ( Category._≈_ A ) 
+
+
+MaybeCat : Category   c₁ (ℓ ⊔ c₂)  (ℓ ⊔ c₂)
+MaybeCat =   record {
+    Obj  = Obj A  ;
+    Hom = λ a b →   MaybeHom A  a b   ; 
+    _o_ =  _×_   ;
+    _≈_ = λ a b →    _==_ (hom a) (hom b)  ;
+    Id  =  \{a} -> MaybeHomId a ;
+    isCategory  = record {
+            isEquivalence = record {refl = *refl ; trans = ? ; sym = ? };
+            identityL  = \{a b f} -> {!!} {a} {b} {f} ;
+            identityR  = \{a b f} -> {!!} {a} {b} {f} ;
+            o-resp-≈  = \{a b c f g h i} -> {!!}  {a} {b} {c} {f} {g} {h} {i} ;
+            associative  = \{a b c d f g h } -> {!!}  {a} {b} {c} {d} {f} {g} {h}
+       } 
+   } where
+        open ≈-Reasoning (A) 
+
+        *refl :   {a b : Obj A } -> {x : Maybe ( Hom A a b ) } → x == x
+        *refl  {_} {_} {just x}  = just refl-hom
+        *refl  {_} {_} {nothing} = nothing
+
+        *sym : ∀ {x y} → x == y → y == x
+        *sym (just x≈y) = just (sym x≈y)
+        *sym nothing    = nothing
+
+        *trans : ∀ {x y z} → x == y → y == z → x == z
+        *trans (just x≈y) (just y≈z) = just (trans-hom x≈y y≈z)
+        *trans nothing    nothing    = nothing
+