Mercurial > hg > Members > kono > Proof > category

changeset 380:c2ca1443bc1d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 12 Mar 2016 13:15:53 +0900
parents 44f045fcbd20
children 1ae9a3fcb0ee
files limit-to.agda
diffstat 1 files changed, 7 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- 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} {_} {_} _ _ = {!!}