Mercurial > hg > Members > kono > Proof > category
changeset 26:ad62c87659ef
join association finish
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 12 Jul 2013 20:45:54 +0900 |
| parents | 8117bafdec7a |
| children | d9c2386a18a8 |
| files | nat.agda |
| diffstat | 1 files changed, 4 insertions(+), 5 deletions(-) [+] |
line wrap: on
line diff
--- a/nat.agda Fri Jul 12 20:32:19 2013 +0900 +++ b/nat.agda Fri Jul 12 20:45:54 2013 +0900 @@ -300,15 +300,14 @@ A [ A [ Trans μ d o A [ A [ FMap T h o Trans μ c ] o FMap T g ] ] o f ] ≈⟨ car-eq f assoc ⟩ A [ A [ A [ Trans μ d o A [ FMap T h o Trans μ c ] ] o FMap T g ] o f ] --- ≈⟨ car-eq f (cdr-eq ( Trans μ d ) ( sym ( nat A μ))) ⟩ ≈⟨ car-eq f (car-eq ( FMap T g) ( cdr-eq ( Trans μ d ) ( begin - {!!} - ≈⟨ {!!} ⟩ - {!!} + A [ FMap T h o Trans μ c ] + ≈⟨ nat A μ ⟩ + A [ Trans μ (FObj T d) o FMap T (FMap T h) ] ∎ ))) ⟩ A [ A [ A [ Trans μ d o A [ Trans μ ( FObj T d) o FMap T ( FMap T h ) ] ] o FMap T g ] o f ] - ≈⟨ {!!} ⟩ + ≈⟨ car-eq f (sym assoc) ⟩ A [ A [ Trans μ d o A [ A [ Trans μ ( FObj T d) o FMap T ( FMap T h ) ] o FMap T g ] ] o f ] ≈⟨ car-eq f ( cdr-eq ( Trans μ d ) (sym assoc) ) ⟩ A [ A [ Trans μ d o A [ Trans μ ( FObj T d) o A [ FMap T ( FMap T h ) o FMap T g ] ] ] o f ]