Mercurial > hg > Members > kono > Proof > category
changeset 63:97eb12318048
cleanup
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 25 Jul 2013 12:09:01 +0900 |
| parents | c5277284919e |
| children | 007d0c6e5d88 |
| files | nat.agda |
| diffstat | 1 files changed, 17 insertions(+), 14 deletions(-) [+] |
line wrap: on
line diff
--- a/nat.agda Thu Jul 25 11:43:51 2013 +0900 +++ b/nat.agda Thu Jul 25 12:09:01 2013 +0900 @@ -219,7 +219,7 @@ -- { η : NTrans A A identityFunctor T } -- { μ : NTrans A A (T ○ T) T } -- ( m : Monad A T η μ ) --- { k : Kleisli A T η μ m} -> +-- { k : Kleisli A T η μ m} → -- IsCategory ( Obj A ) ( Hom A ) ( Category._≈_ A ) ( Kleisli-join ) Kleisli-id -- isKleisliCategory A {T} {η} m = record { isEquivalence = IsCategory.isEquivalence ( Category.isCategory A ) -- ; identityL = {!!} @@ -230,7 +230,7 @@ -- where -- KidL : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) { T : Functor A A } -- { η : NTrans A A identityFunctor T } --- { μ : NTrans A A (T ○ T) T } ( m : Monad A T η μ ) -> {!!} +-- { μ : NTrans A A (T ○ T) T } ( m : Monad A T η μ ) → {!!} -- KidL = {!!} -- KidR : {!!} -- KidR = {!!} @@ -256,21 +256,24 @@ -- } -- } -open Adjunction +---- +-- +-- Adjunction to Monad +-- +---- -lemma11 : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} {A : Category c₁ c₂ ℓ} {B : Category c₁' c₂' ℓ'} - ( U : Functor B A ) ( F : Functor A B ) -> NTrans A A ( U ○ ((F ○ U) ○ F )) ( U ○ (identityFunctor ○ F) ) - -> NTrans A A (( U ○ F ) ○ ( U ○ F )) ( U ○ F ) -lemma11 U F n = record { TMap = \a -> TMap n a; isNTrans = record { naturality = IsNTrans.naturality ( isNTrans n ) }} +open Adjunction UεF : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') ( U : Functor B A ) ( F : Functor A B ) ( ε : NTrans B B ( F ○ U ) identityFunctor ) → NTrans A A (( U ○ F ) ○ ( U ○ F )) ( U ○ F ) -UεF A B U F ε = lemma11 U F ( - Functor*Nat A {B} A U {( F ○ U) ○ F} {identityFunctor ○ F} ( Nat*Functor A {B} B { F ○ U} {identityFunctor} ε F) ) +UεF A B U F ε = lemma11 ( + Functor*Nat A {B} A U {( F ○ U) ○ F} {identityFunctor ○ F} ( Nat*Functor A {B} B { F ○ U} {identityFunctor} ε F) ) where + lemma11 : NTrans A A ( U ○ ((F ○ U) ○ F )) ( U ○ (identityFunctor ○ F) ) + → NTrans A A (( U ○ F ) ○ ( U ○ F )) ( U ○ F ) + lemma11 n = record { TMap = \a → TMap n a; isNTrans = record { naturality = IsNTrans.naturality ( isNTrans n ) }} --- ( \b -> FMap U ( TMap ε ( FObj F b)) ) Adj2Monad : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') { U : Functor B A } { F : Functor A B } @@ -288,9 +291,9 @@ T = U ○ F μ : NTrans A A ( T ○ T ) T μ = UεF A B U F ε - lemma-assoc1 : (b : Obj B) → B [ B [ TMap ε b o TMap ε ( FObj F ( FObj U b)) ] ≈ - B [ TMap ε b o FMap F (FMap U (TMap ε b)) ] ] - lemma-assoc1 b = IsNTrans.naturality ( isNTrans ε ) + lemma-assoc1 : {a b : Obj B} → ( f : Hom B a b) → + B [ B [ f o TMap ε a ] ≈ B [ TMap ε b o FMap F (FMap U f ) ] ] + lemma-assoc1 f = IsNTrans.naturality ( isNTrans ε ) assoc1 : {a : Obj A} → A [ A [ TMap μ a o TMap μ ( FObj T a ) ] ≈ A [ TMap μ a o FMap T (TMap μ a) ] ] assoc1 {a} = let open ≈-Reasoning (A) in begin @@ -299,7 +302,7 @@ (FMap U (TMap ε ( FObj F a ))) o (FMap U (TMap ε ( FObj F ( FObj U (FObj F a ))))) ≈⟨ sym (IsFunctor.distr (isFunctor U)) ⟩ FMap U (B [ TMap ε ( FObj F a ) o TMap ε ( FObj F ( FObj U (FObj F a ))) ] ) - ≈⟨ (IsFunctor.≈-cong (isFunctor U)) (lemma-assoc1 ( FObj F a )) ⟩ + ≈⟨ (IsFunctor.≈-cong (isFunctor U)) (lemma-assoc1 ( TMap ε (FObj F a ))) ⟩ FMap U (B [ (TMap ε ( FObj F a )) o FMap F (FMap U (TMap ε ( FObj F a ))) ] ) ≈⟨ IsFunctor.distr (isFunctor U) ⟩ (FMap U (TMap ε ( FObj F a ))) o FMap U (FMap F (FMap U (TMap ε ( FObj F a ))))