Mercurial > hg > Members > kono > Proof > category

changeset 408:b265e02b0e0b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
if enumarate all possible combination in assoc, it'll pass.
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 22 Mar 2016 15:01:47 +0900
parents 7bdc93de2d6e
children cb03612d8162
files limit-to.agda
diffstat 1 files changed, 14 insertions(+), 30 deletions(-) [+]
line wrap: on
line diff
--- a/limit-to.agda	Mon Mar 21 21:08:46 2016 +0900
+++ b/limit-to.agda	Tue Mar 22 15:01:47 2016 +0900
@@ -36,19 +36,15 @@
 
 -- arrow composition
 
-twocomp : {c₁  c₂ : Level } ->  { a b c : TwoObject {c₁} } ->  Arrow  { c₂ }  ->  Arrow  { c₂ }  ->  Maybe ( Arrow  { c₂ }  )
-twocomp {_} {_} {t0} {t1} {t1} id-t1  arrow-f  = just arrow-f
-twocomp {_} {_} {t0} {t1} {t1} id-t1  arrow-g  = just arrow-g
-twocomp {_} {_} {t1} {t1} {t1} id-t1  id-t1  = just id-t1
-twocomp {_} {_} {t0} {t0} {t1} arrow-f  id-t0 = just arrow-f
-twocomp {_} {_} {t0} {t0} {t1} arrow-g  id-t0 = just arrow-g
-twocomp {_} {_} {t0} {t0} {t0} id-t0  id-t0 = just id-t0
-twocomp _ _ = nothing
 
 _×_ :  { c₁  c₂ : Level }  -> {A B C : TwoObject { c₁} } →  Maybe ( Arrow   { c₂ }) →  Maybe ( Arrow    { c₂ })  →  Maybe ( Arrow  { c₂ })  
 _×_   nothing _  = nothing
 _×_   _ nothing  = nothing
-_×_   { c₁} { c₂} {a} {b} {c} (just f)  (just g)   =  twocomp  { c₁} { c₂} {a} {b} {c} f g  
+_×_   { c₁} { c₂} {t1} {t1} {t1} (just id-t1)  (just id-t1)   =  just id-t1
+_×_   { c₁} { c₂} {t0} {t1} {t1} (just id-t1)  (just f)   =  just f
+_×_   { c₁} { c₂} {t0} {t0} {t0} (just id-t0)  (just id-t0)   =  just id-t0
+_×_   { c₁} { c₂} {t0} {t0} {t1} (just f) (just id-t1)     =  just f
+_×_   { c₁} { c₂} {a} {b} {c} (just f)  (just g)   =  nothing
 
 
 [_==_] : { c₁ c₂ : Level}   {a b : TwoObject {c₁} } ->  Rel (Maybe (Arrow  { c₂ })) (c₂) 
@@ -58,29 +54,17 @@
 --       d <- c <- b <- a
 
 assoc-× :   { c₁  c₂ : Level } {a b c d : TwoObject  { c₁} } {f g h : Maybe (Arrow  { c₂ })} → 
-   [ f × (g × h) == (f × g) × h ]
+     [_==_] { c₁} { c₂} {a} {d}  (  _×_ { c₁} { c₂} {a} {b} {d} f ( _×_ { c₁} { c₂} {a} {b} {c} g h )  )
+                (  _×_ { c₁} { c₂} {a} {c} {d}  ( _×_ { c₁} { c₂} {b} {c} {d} f g )   h )
+--    [ f × (g × h) == (f × g) × h ]
 assoc-× {_} {_} {_} {_} {_} {_} {nothing} {_} {_} = nothing
 assoc-× {_} {_} {_} {_} {_} {_} {just _} {nothing} {_} = nothing
-assoc-× {_} {_} {_} {_} {_} {_} {just _} {just _} {nothing} = nothing
-assoc-× {_} {_} {_} {_} {_} {_} {just f} {just g} {just h} with ((just g ) × (just h)) | ((just f ) × (just g)  )
-... | nothing | _ = nothing
-... | just _ | nothing = nothing
-... | just id-t0 | just id-t0 = just refl
-... | just id-t1 | just id-t1 = just refl
-... | just id-t1 | just arrow-f = just refl
-... | just id-t1 | just arrow-g = just refl
-... | just arrow-f | just id-t0  = just refl
-... | just arrow-g | just id-t0  = just refl
-... | just id-t0 | just id-t1 = nothing
-... | just id-t0 | (just arrow-f) = nothing
-... | just id-t0 | (just arrow-g) = nothing
-... | just id-t1 | (just id-t0) = nothing
-... | just arrow-f | (just id-t1) = nothing
-... | just arrow-f | (just arrow-f) = nothing
-... | just arrow-f | (just arrow-g) = nothing
-... | just arrow-g | (just id-t1) = nothing
-... | just arrow-g | (just arrow-f) = nothing
-... | just arrow-g | (just arrow-g) = nothing
+assoc-× {_} {_} {t0} {t0} {t0} {t0} {just id-t0} {just id-t0} {nothing} = nothing
+assoc-× {_} {_} {_} {_} {_} {_} {just _} {just _} {nothing} = {!!}
+assoc-× {_} {_} {t0} {t0} {t0} {t0} {just id-t0 } {just id-t0 } {just id-t0 } = just refl
+assoc-× {_} {_} {t0} {t0} {t0} {t1} {just id-t0 } {just id-t0 } {just id-t0 } = nothing
+assoc-× {_} {_} {_} {_} {_} {_} {just id-t0 } {just id-t0 } {just id-t0 } = ?
+assoc-× {_} {_} {_} {_} {_} {_} {_} {_} {_} = {!!}
 
 TwoId :  { c₁  c₂ : Level } {a : TwoObject  { c₁} } ->  Maybe (Arrow  { c₂ })
 TwoId {_} {_} {t0} = just id-t0