Mercurial > hg > Members > kono > Proof > category
changeset 28:5289c46d8eef
fix
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 13 Jul 2013 03:05:43 +0900 |
| parents | d9c2386a18a8 |
| children | 87cefecc5663 |
| files | nat.agda |
| diffstat | 1 files changed, 47 insertions(+), 44 deletions(-) [+] |
line wrap: on
line diff
--- a/nat.agda Fri Jul 12 22:17:23 2013 +0900 +++ b/nat.agda Sat Jul 13 03:05:43 2013 +0900 @@ -144,13 +144,13 @@ -- some short cuts - car-eq : {a b c : Obj A } {x y : Hom A a b } ( f : Hom A c a ) → + car : {a b c : Obj A } {x y : Hom A a b } { f : Hom A c a } → A [ x ≈ y ] → A [ A [ x o f ] ≈ A [ y o f ] ] - car-eq f eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) ( refl-hom ) eq + car {f} eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) ( refl-hom ) eq - cdr-eq : {a b c : Obj A } {x y : Hom A a b } ( f : Hom A b c ) → + cdr : {a b c : Obj A } {x y : Hom A a b } { f : Hom A b c } → A [ x ≈ y ] → A [ A [ f o x ] ≈ A [ f o y ] ] - cdr-eq f eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) eq (refl-hom ) + cdr {f} eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) eq (refl-hom ) id : (a : Obj A ) → Hom A a a id a = (Id {_} {_} {_} {A} a) @@ -177,6 +177,9 @@ → A [ A [ ( FMap G f ) o ( Trans η a ) ] ≈ A [ (Trans η b ) o (FMap F f) ] ] nat _ η = IsNTrans.naturality ( isNTrans η ) + _o_ : {a b c : Obj A } ( x : Hom A a b ) ( y : Hom A c a ) -> Hom A c b + x o y = A [ x o y ] + infixr 2 _∎ infixr 2 _≈⟨_⟩_ infix 1 begin_ @@ -239,7 +242,7 @@ c [ Trans μ b o c [ FMap T ((Trans η b)) o f ] ] ≈⟨ IsCategory.associative (Category.isCategory c) ⟩ c [ c [ Trans μ b o FMap T ((Trans η b)) ] o f ] - ≈⟨ car-eq f ( IsMonad.unity2 ( isMonad ( monad k )) ) ⟩ + ≈⟨ car ( IsMonad.unity2 ( isMonad ( monad k )) ) ⟩ c [ id (FObj T b) o f ] ≈⟨ IsCategory.identityL (Category.isCategory c) ⟩ f @@ -260,11 +263,11 @@ join k b f (Trans η a) ≈⟨ refl-hom ⟩ c [ Trans μ b o c [ FMap T f o (Trans η a) ] ] - ≈⟨ cdr-eq (Trans μ b) ( IsNTrans.naturality ( isNTrans η )) ⟩ + ≈⟨ cdr ( IsNTrans.naturality ( isNTrans η )) ⟩ c [ Trans μ b o c [ (Trans η ( FObj T b)) o f ] ] ≈⟨ IsCategory.associative (Category.isCategory c) ⟩ c [ c [ Trans μ b o (Trans η ( FObj T b)) ] o f ] - ≈⟨ car-eq f ( IsMonad.unity1 ( isMonad ( monad k )) ) ⟩ + ≈⟨ car ( IsMonad.unity1 ( isMonad ( monad k )) ) ⟩ c [ id (FObj T b) o f ] ≈⟨ IsCategory.identityL (Category.isCategory c) ⟩ f @@ -287,53 +290,53 @@ Lemma9 A T η μ a b c d f g h m k = begin join k d h (join k c g f) - ≈⟨ refl-hom ⟩ - 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 o A [ g o h ] ] = A [ A [ f o g ] o h ] - A [ A [ Trans μ d o FMap T h ] o A [ A [ Trans μ c o FMap T g ] o f ] ] + ≈⟨ refl-hom ⟩ + join k d h ( ( Trans μ c o ( FMap T g o f ) ) ) + ≈⟨ refl-hom ⟩ + ( Trans μ d o ( FMap T h o ( Trans μ c o ( FMap T g o f ) ) ) ) + ≈⟨ cdr ( cdr ( assoc )) ⟩ + ( Trans μ d o ( FMap T h o ( ( Trans μ c o FMap T g ) o f ) ) ) + ≈⟨ assoc ⟩ --- ( f o ( g o h ) ) = ( ( f o g ) o h ) + ( ( Trans μ d o FMap T h ) o ( (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 (car-eq ( FMap T g) ( cdr-eq ( Trans μ d ) ( begin - A [ FMap T h o Trans μ c ] + ( ( ( Trans μ d o FMap T h ) o (Trans μ c o FMap T g ) ) o f ) + ≈⟨ car (sym assoc) ⟩ + ( ( Trans μ d o ( FMap T h o ( Trans μ c o FMap T g ) ) ) o f ) + ≈⟨ car ( cdr (assoc) ) ⟩ + ( ( Trans μ d o ( ( FMap T h o Trans μ c ) o FMap T g ) ) o f ) + ≈⟨ car assoc ⟩ + ( ( ( Trans μ d o ( FMap T h o Trans μ c ) ) o FMap T g ) o f ) + ≈⟨ car (car ( cdr ( begin + ( FMap T h o Trans μ c ) ≈⟨ nat A μ ⟩ - A [ Trans μ (FObj T d) o FMap T (FMap T h) ] + ( 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 ] - ≈⟨ 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 ] )) ( + ( ( ( Trans μ d o ( Trans μ ( FObj T d) o FMap T ( FMap T h ) ) ) o FMap T g ) o f ) + ≈⟨ car (sym assoc) ⟩ + ( ( Trans μ d o ( ( Trans μ ( FObj T d) o FMap T ( FMap T h ) ) o FMap T g ) ) o f ) + ≈⟨ car ( cdr (sym assoc) ) ⟩ + ( ( Trans μ d o ( Trans μ ( FObj T d) o ( FMap T ( FMap T h ) o FMap T g ) ) ) o f ) + ≈⟨ car ( cdr (cdr (sym (distr T )))) ⟩ + ( ( Trans μ d o ( Trans μ ( FObj T d) o FMap T ( ( FMap T h o g ) ) ) ) o f ) + ≈⟨ car assoc ⟩ + ( ( ( Trans μ d o Trans μ ( FObj T d) ) o FMap T ( ( FMap T h o g ) ) ) o f ) + ≈⟨ car ( car ( begin - A [ Trans μ d o Trans μ (FObj T d) ] + ( Trans μ d o Trans μ (FObj T d) ) ≈⟨ IsMonad.assoc ( isMonad m) ⟩ - A [ Trans μ d o FMap T (Trans μ d) ] + ( Trans μ d o FMap T (Trans μ d) ) ∎ )) ⟩ - 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 ] + ( ( ( Trans μ d o FMap T ( Trans μ d) ) o FMap T ( ( FMap T h o g ) ) ) o f ) + ≈⟨ car (sym assoc) ⟩ + ( ( Trans μ d o ( FMap T ( Trans μ d ) o FMap T ( ( FMap T h o g ) ) ) ) o f ) ≈⟨ sym assoc ⟩ - A [ Trans μ d o A [ A [ FMap T ( Trans μ d ) o FMap T ( A [ FMap T h o g ] ) ] o f ] ] - ≈⟨ cdr-eq ( Trans μ d ) ( car-eq f ( sym ( distr T ))) ⟩ - A [ Trans μ d o A [ FMap T ( A [ ( Trans μ d ) o A [ FMap T h o g ] ] ) o f ] ] + ( Trans μ d o ( ( FMap T ( Trans μ d ) o FMap T ( ( FMap T h o g ) ) ) o f ) ) + ≈⟨ cdr ( car ( sym ( distr T ))) ⟩ + ( Trans μ d o ( FMap T ( ( ( Trans μ d ) o ( FMap T h o g ) ) ) o f ) ) ≈⟨ refl-hom ⟩ - join k d ( A [ Trans μ d o A [ FMap T h o g ] ] ) f + join k d ( ( Trans μ d o ( FMap T h o g ) ) ) f ≈⟨ refl-hom ⟩ join k d ( join k d h g) f ∎ where open ≈-Reasoning (A)