Mercurial > hg > Members > kono > Proof > category
changeset 25:8117bafdec7a
on going
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 12 Jul 2013 20:32:19 +0900 |
| parents | 171c31acf78e |
| children | ad62c87659ef |
| files | nat.agda |
| diffstat | 1 files changed, 27 insertions(+), 2 deletions(-) [+] |
line wrap: on
line diff
--- a/nat.agda Fri Jul 12 18:58:16 2013 +0900 +++ b/nat.agda Fri Jul 12 20:32:19 2013 +0900 @@ -288,10 +288,35 @@ join k d h ( A [ Trans μ c o A [ FMap T g o f ] ] ) ≈⟨ refl-hom ⟩ A [ Trans μ d o A [ FMap T h o A [ Trans μ c o A [ FMap T g o f ] ] ] ] + ≈⟨ cdr-eq ( Trans μ d ) ( cdr-eq ( FMap T h ) ( assoc )) ⟩ + A [ Trans μ d o A [ FMap T h o A [ A [ Trans μ c o FMap T g ] o f ] ] ] + ≈⟨ assoc ⟩ --- A [ f x A [ g x h ] ] = A [ A [ f x g ] x h ] + A [ A [ Trans μ d o FMap T h ] o A [ A [ Trans μ c o FMap T g ] o f ] ] + ≈⟨ assoc ⟩ + A [ A [ A [ Trans μ d o FMap T h ] o A [ Trans μ c o FMap T g ] ] o f ] + ≈⟨ car-eq f (sym assoc) ⟩ + A [ A [ Trans μ d o A [ FMap T h o A [ Trans μ c o FMap T g ] ] ] o f ] + ≈⟨ car-eq f ( cdr-eq ( Trans μ d ) (assoc) ) ⟩ + 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 [ A [ A [ Trans μ d o A [ Trans μ ( FObj T d) o FMap T ( FMap T h ) ] ] o FMap T g ] o f ] ≈⟨ {!!} ⟩ --- ≈⟨ cdr-eq ( Trans μ d ) ( nat A μ) ⟩ + 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 ] + ≈⟨ car-eq f ( cdr-eq ( Trans μ d) (cdr-eq (Trans μ ( FObj T d) ) (sym (distr T )))) ⟩ + A [ A [ Trans μ d o A [ Trans μ ( FObj T d) o FMap T ( A [ FMap T h o g ] ) ] ] o f ] + ≈⟨ car-eq f assoc ⟩ A [ A [ A [ Trans μ d o Trans μ ( FObj T d) ] o FMap T ( A [ FMap T h o g ] ) ] o f ] - ≈⟨ ⟩ + ≈⟨ car-eq f ( car-eq (FMap T ( A [ FMap T h o g ] )) ( IsMonad.assoc ( isMonad m ))) ⟩ A [ A [ A [ Trans μ d o FMap T ( Trans μ d) ] o FMap T ( A [ FMap T h o g ] ) ] o f ] ≈⟨ car-eq f (sym assoc) ⟩ A [ A [ Trans μ d o A [ FMap T ( Trans μ d ) o FMap T ( A [ FMap T h o g ] ) ] ] o f ]