# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1457756153 -32400
# Node ID c2ca1443bc1d59e101a6f96b7d072225fd4cddcd
# Parent  44f045fcbd202931349d414ec1a1ae69e715a038
fix

diff -r 44f045fcbd20 -r c2ca1443bc1d limit-to.agda
--- a/limit-to.agda	Sat Mar 12 12:33:31 2016 +0900
+++ b/limit-to.agda	Sat Mar 12 13:15:53 2016 +0900
@@ -135,6 +135,12 @@
 --         identityR {t0} {t1} {f} = refl
 --         identityR {t1} {t0} {f} = selection f
 --         identityR {t1} {t1} {f} = selection f
+        nothing-eq : {A B : TwoObject} {f : Maybe ( Two-Hom A B)} ->  twomap f ≡ nothing -> f ≡ nothing
+        nothing-eq {_} {_} {nothing } eq = refl
+        nothing-eq {t0} {t0} {just f} eq = ?
+        nothing-eq {t0} {t1} {just f} eq = ?
+        nothing-eq {t1} {t0} {just f} eq = ?
+        nothing-eq {t1} {t1} {just f} eq = ?
         o-resp-≈ : {A B C : TwoObject} {f g : Maybe ( Two-Hom A B)} {h i : Maybe (Two-Hom B C)} →
             twomap f ≡ twomap g → twomap h ≡ twomap i → twomap ( h × f ) ≡ twomap ( i × g )
         o-resp-≈  {a} {b} {c} {nothing} {g} {h} {i}  f≡g  h≡i   =  let open ≡-Reasoning in
@@ -144,7 +150,7 @@
                 nothing
               ≡⟨⟩
                 twomap {a} {c} (i × nothing)
-              ≡⟨ f≡g ⟩
+              ≡⟨ {!!} f≡g ⟩
                 twomap (i × g)
               ∎
         o-resp-≈  {_} {_} {_} {_} {nothing} {_} {_} _ _ = {!!}