--- a/maybeCat.agda	Thu Mar 24 13:11:50 2016 +0900
+++ b/maybeCat.agda	Thu Mar 24 13:44:27 2016 +0900
@@ -6,6 +6,7 @@
 open import cat-utility
 open import HomReasoning
 open import Relation.Binary 
+open import Relation.Binary.Core
 open import Data.Maybe
 
 open Functor
@@ -48,6 +49,10 @@
         ≡≡-trans (just x≈y) (just y≈z) = just (trans-hom x≈y y≈z)  where  open ≈-Reasoning (A)
         ≡≡-trans nothing    nothing    = nothing
 
+        ≡≡-cong :  ∀{ a b c d }   -> ∀ {x y :  Maybe (Hom A a b )} →
+                (f : Maybe (Hom A a b ) -> Maybe (Hom A c d ) )  ->  x  ≡  y  →  A [ f x ≡≡ f y ]
+        ≡≡-cong  {a} {b } {c} {d} {nothing} {nothing} f refl  = ≡≡-refl
+        ≡≡-cong  {a} {b } {c} {d} {just x} {just .x} f refl  = ≡≡-refl
 
         data _IsRelatedTo_  {a b : Obj A}  (x y : (Maybe (Hom A a b ))) :
                              Set  (ℓ ⊔ c₂)  where