Mercurial > hg > Members > kono > Proof > category

changeset 362:c18b209a662a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
member
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 26 Jun 2015 19:38:57 +0900
parents e9d4e6ab6cd1
children cf9ee72f9b0e
files limit-to.agda
diffstat 1 files changed, 8 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/limit-to.agda	Fri Jun 26 19:18:57 2015 +0900
+++ b/limit-to.agda	Fri Jun 26 19:38:57 2015 +0900
@@ -111,13 +111,15 @@
 -- arrow composition
 
 _×_ :  {A B C : Two} → Two-Hom B C → Two-Hom A B → Two-Hom A C
-_×_  {t0} {t0} {t0} a b  = {!!}
-_×_  {t0} {t0} {t1} a b  = {!!}
-_×_  {t0} {t1} {t0} a b  = {!!}
-_×_  {t0} {t1} {t1} a b  = {!!}
-_×_  {t1} {t0} {t1} a b  = {!!}
+_×_  {t0} {t0} {t0} a b  = record { Map = id-0; isMap = refl }
+_×_  {t0} {t0} {t1} a b  =  record { Map = {!!} ; isMap = refl }
+_×_  {t0} {t1} {t1} a b  =   record { Map =  {!!} ; isMap = refl }
+_×_  {t1} {t1} {t1} a b  =   record { Map = id-1; isMap = refl }
+-- not happening case, but we have possible answer
+_×_  {t0} {t1} {t0} a b  =  record { Map = id-0; isMap = refl }
+_×_  {t1} {t0} {t1} a b  =  record { Map = id-1; isMap = refl }
+-- non exiting arrow ( how to handle it? ) we cannot create the answer ...
 _×_  {t1} {t0} {t0} a b  = {!!}
-_×_  {t1} {t1} {t1} a b  = {!!}
 _×_  {t1} {t1} {t0} a b  = {!!}