Mercurial > hg > Members > kono > Proof > category

comparison CCCGraph1.agda @ 835:3bdb93608aae

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 26 Mar 2020 16:44:06 +0900
parents b25fcdf3a84a
children 861cae4707bd
comparison
equal deleted inserted replaced
834:b25fcdf3a84a 835:3bdb93608aae
50 eval {a} {_} {⊤} _ _ = i ( ○ a ) 50 eval {a} {_} {⊤} _ _ = i ( ○ a )
51 eval f (i k) = eval1 f k 51 eval f (i k) = eval1 f k
52 eval (id _) f = f 52 eval (id _) f = f
53 eval π (iii g h) = g 53 eval π (iii g h) = g
54 eval π' (iii g h) = h 54 eval π' (iii g h) = h
55 eval ε (iii g h) = {!!} -- {!!} ・ h -- g : Arrows a (c <= b) 55 eval ε (iii (i k) (i h)) = iv (i ε) < k , h >
56 eval ε (iii (i k) h) = iv ( iv (i ε) < k , {!!} > ) {!!}
57 eval ε (iii (iv f g) h) = {!!}
58 eval ε (iii (v g) h) = {!!} -- {!!} ・ h -- g : Arrows a (c <= b)
56 eval < f , g > (iii j h) = iii (eval f (iii j h)) (eval g (iii j h)) 59 eval < f , g > (iii j h) = iii (eval f (iii j h)) (eval g (iii j h))
57 eval (f *) (iii g h) = {!!} 60 eval (f *) (iii g h) = {!!}
58 eval f (iv g h) with eval f g 61 eval f (iv g h) with eval f g
59 ... | i k = eval1 k h 62 ... | i k = eval1 k h
60 ... | k = iv k h 63 ... | k = iv k h