Mercurial > hg > Members > kono > Proof > category
changeset 87:4690953794c4
MEsolution
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 28 Jul 2013 08:04:01 +0900 |
| parents | be4e3b073e0d |
| children | 419923b149ca |
| files | cat-utility.agda nat.agda |
| diffstat | 2 files changed, 144 insertions(+), 144 deletions(-) [+] |
line wrap: on
line diff
--- a/cat-utility.agda Sat Jul 27 21:19:58 2013 +0900 +++ b/cat-utility.agda Sun Jul 28 08:04:01 2013 +0900 @@ -2,145 +2,145 @@ -- Shinji KONO <kono@ie.u-ryukyu.ac.jp> -open import Category -- https://github.com/konn/category-agda -open import Level ---open import Category.HomReasoning -open import HomReasoning + open import Category -- https://github.com/konn/category-agda + open import Level + --open import Category.HomReasoning + open import HomReasoning -open Functor + open Functor -id1 : ∀{c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (a : Obj A ) → Hom A a a -id1 A a = (Id {_} {_} {_} {A} a) + id1 : ∀{c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (a : Obj A ) → Hom A a a + id1 A a = (Id {_} {_} {_} {A} a) -record IsUniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') - ( U : Functor B A ) - ( F : Obj A → Obj B ) - ( η : (a : Obj A) → Hom A a ( FObj U (F a) ) ) - ( _* : { a : Obj A}{ b : Obj B} → ( Hom A a (FObj U b) ) → Hom B (F a ) b ) - : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where - field - universalMapping : {a' : Obj A} { b' : Obj B } → { f : Hom A a' (FObj U b') } → - A [ A [ FMap U ( f * ) o η a' ] ≈ f ] - uniquness : {a' : Obj A} { b' : Obj B } → { f : Hom A a' (FObj U b') } → { g : Hom B (F a') b' } → - A [ A [ FMap U g o η a' ] ≈ f ] → B [ f * ≈ g ] + record IsUniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') + ( U : Functor B A ) + ( F : Obj A → Obj B ) + ( η : (a : Obj A) → Hom A a ( FObj U (F a) ) ) + ( _* : { a : Obj A}{ b : Obj B} → ( Hom A a (FObj U b) ) → Hom B (F a ) b ) + : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where + field + universalMapping : {a' : Obj A} { b' : Obj B } → { f : Hom A a' (FObj U b') } → + A [ A [ FMap U ( f * ) o η a' ] ≈ f ] + uniquness : {a' : Obj A} { b' : Obj B } → { f : Hom A a' (FObj U b') } → { g : Hom B (F a') b' } → + A [ A [ FMap U g o η a' ] ≈ f ] → B [ f * ≈ g ] -record UniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') - ( U : Functor B A ) - ( F : Obj A → Obj B ) - ( η : (a : Obj A) → Hom A a ( FObj U (F a) ) ) - : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where - infixr 11 _* - field - _* : { a : Obj A}{ b : Obj B} → ( Hom A a (FObj U b) ) → Hom B (F a ) b - isUniversalMapping : IsUniversalMapping A B U F η _* + record UniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') + ( U : Functor B A ) + ( F : Obj A → Obj B ) + ( η : (a : Obj A) → Hom A a ( FObj U (F a) ) ) + : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where + infixr 11 _* + field + _* : { a : Obj A}{ b : Obj B} → ( Hom A a (FObj U b) ) → Hom B (F a ) b + isUniversalMapping : IsUniversalMapping A B U F η _* -open NTrans -open import Category.Cat -record IsAdjunction {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') - ( U : Functor B A ) - ( F : Functor A B ) - ( η : NTrans A A identityFunctor ( U ○ F ) ) - ( ε : NTrans B B ( F ○ U ) identityFunctor ) - : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where - field - adjoint1 : { b : Obj B } → - A [ A [ ( FMap U ( TMap ε b )) o ( TMap η ( FObj U b )) ] ≈ id1 A (FObj U b) ] - adjoint2 : {a : Obj A} → - B [ B [ ( TMap ε ( FObj F a )) o ( FMap F ( TMap η a )) ] ≈ id1 B (FObj F a) ] + open NTrans + open import Category.Cat + record IsAdjunction {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') + ( U : Functor B A ) + ( F : Functor A B ) + ( η : NTrans A A identityFunctor ( U ○ F ) ) + ( ε : NTrans B B ( F ○ U ) identityFunctor ) + : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where + field + adjoint1 : { b : Obj B } → + A [ A [ ( FMap U ( TMap ε b )) o ( TMap η ( FObj U b )) ] ≈ id1 A (FObj U b) ] + adjoint2 : {a : Obj A} → + B [ B [ ( TMap ε ( FObj F a )) o ( FMap F ( TMap η a )) ] ≈ id1 B (FObj F a) ] -record Adjunction {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') - ( U : Functor B A ) - ( F : Functor A B ) - ( η : NTrans A A identityFunctor ( U ○ F ) ) - ( ε : NTrans B B ( F ○ U ) identityFunctor ) - : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where - field - isAdjunction : IsAdjunction A B U F η ε + record Adjunction {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') + ( U : Functor B A ) + ( F : Functor A B ) + ( η : NTrans A A identityFunctor ( U ○ F ) ) + ( ε : NTrans B B ( F ○ U ) identityFunctor ) + : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where + field + isAdjunction : IsAdjunction A B U F η ε -record IsMonad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) - ( T : Functor A A ) - ( η : NTrans A A identityFunctor T ) - ( μ : NTrans A A (T ○ T) T) - : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where - field - assoc : {a : Obj A} → A [ A [ TMap μ a o TMap μ ( FObj T a ) ] ≈ A [ TMap μ a o FMap T (TMap μ a) ] ] - unity1 : {a : Obj A} → A [ A [ TMap μ a o TMap η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ] - unity2 : {a : Obj A} → A [ A [ TMap μ a o (FMap T (TMap η a ))] ≈ Id {_} {_} {_} {A} (FObj T a) ] + record IsMonad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) + ( T : Functor A A ) + ( η : NTrans A A identityFunctor T ) + ( μ : NTrans A A (T ○ T) T) + : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where + field + assoc : {a : Obj A} → A [ A [ TMap μ a o TMap μ ( FObj T a ) ] ≈ A [ TMap μ a o FMap T (TMap μ a) ] ] + unity1 : {a : Obj A} → A [ A [ TMap μ a o TMap η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ] + unity2 : {a : Obj A} → A [ A [ TMap μ a o (FMap T (TMap η a ))] ≈ Id {_} {_} {_} {A} (FObj T a) ] -record Monad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (T : Functor A A) (η : NTrans A A identityFunctor T) (μ : NTrans A A (T ○ T) T) - : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where - eta : NTrans A A identityFunctor T - eta = η - mu : NTrans A A (T ○ T) T - mu = μ - field - isMonad : IsMonad A T η μ + record Monad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (T : Functor A A) (η : NTrans A A identityFunctor T) (μ : NTrans A A (T ○ T) T) + : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where + eta : NTrans A A identityFunctor T + eta = η + mu : NTrans A A (T ○ T) T + mu = μ + field + isMonad : IsMonad A T η μ -Functor*Nat : {c₁ c₂ ℓ c₁' c₂' ℓ' c₁'' c₂'' ℓ'' : Level} (A : Category c₁ c₂ ℓ) {B : Category c₁' c₂' ℓ'} (C : Category c₁'' c₂'' ℓ'') - (F : Functor B C) -> { G H : Functor A B } -> ( n : NTrans A B G H ) -> NTrans A C (F ○ G) (F ○ H) -Functor*Nat A {B} C F {G} {H} n = record { - TMap = \a -> FMap F (TMap n a) - ; isNTrans = record { - naturality = naturality - } - } where - naturality : {a b : Obj A} {f : Hom A a b} - → C [ C [ (FMap F ( FMap H f )) o ( FMap F (TMap n a)) ] ≈ C [ (FMap F (TMap n b )) o (FMap F (FMap G f)) ] ] - naturality {a} {b} {f} = let open ≈-Reasoning (C) in - begin - (FMap F ( FMap H f )) o ( FMap F (TMap n a)) - ≈⟨ sym (distr F) ⟩ - FMap F ( B [ (FMap H f) o TMap n a ]) - ≈⟨ IsFunctor.≈-cong (isFunctor F) ( nat n ) ⟩ - FMap F ( B [ (TMap n b ) o FMap G f ] ) - ≈⟨ distr F ⟩ - (FMap F (TMap n b )) o (FMap F (FMap G f)) - ∎ + Functor*Nat : {c₁ c₂ ℓ c₁' c₂' ℓ' c₁'' c₂'' ℓ'' : Level} (A : Category c₁ c₂ ℓ) {B : Category c₁' c₂' ℓ'} (C : Category c₁'' c₂'' ℓ'') + (F : Functor B C) -> { G H : Functor A B } -> ( n : NTrans A B G H ) -> NTrans A C (F ○ G) (F ○ H) + Functor*Nat A {B} C F {G} {H} n = record { + TMap = \a -> FMap F (TMap n a) + ; isNTrans = record { + naturality = naturality + } + } where + naturality : {a b : Obj A} {f : Hom A a b} + → C [ C [ (FMap F ( FMap H f )) o ( FMap F (TMap n a)) ] ≈ C [ (FMap F (TMap n b )) o (FMap F (FMap G f)) ] ] + naturality {a} {b} {f} = let open ≈-Reasoning (C) in + begin + (FMap F ( FMap H f )) o ( FMap F (TMap n a)) + ≈⟨ sym (distr F) ⟩ + FMap F ( B [ (FMap H f) o TMap n a ]) + ≈⟨ IsFunctor.≈-cong (isFunctor F) ( nat n ) ⟩ + FMap F ( B [ (TMap n b ) o FMap G f ] ) + ≈⟨ distr F ⟩ + (FMap F (TMap n b )) o (FMap F (FMap G f)) + ∎ -Nat*Functor : {c₁ c₂ ℓ c₁' c₂' ℓ' c₁'' c₂'' ℓ'' : Level} (A : Category c₁ c₂ ℓ) {B : Category c₁' c₂' ℓ'} (C : Category c₁'' c₂'' ℓ'') - { G H : Functor B C } -> ( n : NTrans B C G H ) -> (F : Functor A B) -> NTrans A C (G ○ F) (H ○ F) -Nat*Functor A {B} C {G} {H} n F = record { - TMap = \a -> TMap n (FObj F a) - ; isNTrans = record { - naturality = naturality - } - } where - naturality : {a b : Obj A} {f : Hom A a b} - → C [ C [ ( FMap H (FMap F f )) o ( TMap n (FObj F a)) ] ≈ C [ (TMap n (FObj F b )) o (FMap G (FMap F f)) ] ] - naturality {a} {b} {f} = IsNTrans.naturality ( isNTrans n) + Nat*Functor : {c₁ c₂ ℓ c₁' c₂' ℓ' c₁'' c₂'' ℓ'' : Level} (A : Category c₁ c₂ ℓ) {B : Category c₁' c₂' ℓ'} (C : Category c₁'' c₂'' ℓ'') + { G H : Functor B C } -> ( n : NTrans B C G H ) -> (F : Functor A B) -> NTrans A C (G ○ F) (H ○ F) + Nat*Functor A {B} C {G} {H} n F = record { + TMap = \a -> TMap n (FObj F a) + ; isNTrans = record { + naturality = naturality + } + } where + naturality : {a b : Obj A} {f : Hom A a b} + → C [ C [ ( FMap H (FMap F f )) o ( TMap n (FObj F a)) ] ≈ C [ (TMap n (FObj F b )) o (FMap G (FMap F f)) ] ] + naturality {a} {b} {f} = IsNTrans.naturality ( isNTrans n) -record Kleisli { 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 η μ ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where - monad : Monad A T η μ - monad = M - -- g ○ f = μ(c) T(g) f - join : { a b : Obj A } → { c : Obj A } → - ( Hom A b ( FObj T c )) → ( Hom A a ( FObj T b)) → Hom A a ( FObj T c ) - join {_} {_} {c} g f = A [ TMap μ c o A [ FMap T g o f ] ] + record Kleisli { 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 η μ ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where + monad : Monad A T η μ + monad = M + -- g ○ f = μ(c) T(g) f + join : { a b : Obj A } → { c : Obj A } → + ( Hom A b ( FObj T c )) → ( Hom A a ( FObj T b)) → Hom A a ( FObj T c ) + join {_} {_} {c} g f = A [ TMap μ c o A [ FMap T g o f ] ] --- T ≃ (U_R ○ F_R) --- μ = U_R ε F_R --- nat-ε --- nat-η -- same as η but has different types + -- T ≃ (U_R ○ F_R) + -- μ = U_R ε F_R + -- nat-ε + -- nat-η -- same as η but has different types -record Resolution {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) ( B : Category c₁ c₂ ℓ ) - ( T : Functor A A ) - { η : NTrans A A identityFunctor T } - { μ : NTrans A A (T ○ T) T } - ( M : Monad A T η μ ) - ( UR : Functor B A ) ( FR : Functor A B ) - { ηR : NTrans A A identityFunctor ( UR ○ FR ) } - { εR : NTrans B B ( FR ○ UR ) identityFunctor } - { μR : NTrans A A ( (UR ○ FR) ○ ( UR ○ FR )) ( UR ○ FR ) } - ( Adj : Adjunction A B UR FR ηR εR ) - : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where - field - T=UF : T ≃ (UR ○ FR) - μ=UεF : {x : Obj A } -> A [ TMap μR x ≈ FMap UR ( TMap εR ( FObj FR x ) ) ] - -- ηR=η : {x : Obj A } -> A [ TMap ηR x ≈ TMap η x ] - -- μR=μ : {x : Obj A } -> A [ TMap μR x ≈ TMap μ x ] + record MResolution {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) ( B : Category c₁' c₂' ℓ' ) + ( T : Functor A A ) + { η : NTrans A A identityFunctor T } + { μ : NTrans A A (T ○ T) T } + ( M : Monad A T η μ ) + ( UR : Functor B A ) ( FR : Functor A B ) + { ηR : NTrans A A identityFunctor ( UR ○ FR ) } + { εR : NTrans B B ( FR ○ UR ) identityFunctor } + { μR : NTrans A A ( (UR ○ FR) ○ ( UR ○ FR )) ( UR ○ FR ) } + ( Adj : Adjunction A B UR FR ηR εR ) + : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where + field + T=UF : T ≃ (UR ○ FR) + μ=UεF : {x : Obj A } -> A [ TMap μR x ≈ FMap UR ( TMap εR ( FObj FR x ) ) ] + -- ηR=η : {x : Obj A } -> A [ TMap ηR x ≈ TMap η x ] + -- μR=μ : {x : Obj A } -> A [ TMap μR x ≈ TMap μ x ]
--- a/nat.agda Sat Jul 27 21:19:58 2013 +0900 +++ b/nat.agda Sun Jul 28 08:04:01 2013 +0900 @@ -210,16 +210,19 @@ -- Hom in Kleisli Category -- -record KHom (a : Obj A) (b : Obj A) + +record KleisliHom { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } { T : Functor A A } (a : Obj A) (b : Obj A) : Set c₂ where field KMap : Hom A a ( FObj T b ) +KHom = \(a b : Obj A) -> KleisliHom { c₁} {c₂} {ℓ} {A} {T} a b + K-id : {a : Obj A} → KHom a a K-id {a = a} = record { KMap = TMap η a } open import Relation.Binary.Core -open KHom +open KleisliHom _⋍_ : { a : Obj A } { b : Obj A } (f g : KHom a b ) -> Set ℓ _⋍_ {a} {b} f g = A [ KMap f ≈ KMap g ] @@ -514,7 +517,7 @@ ∎ adjoint2 : {a : Obj A} → KleisliCategory [ KleisliCategory [ ( TMap nat-ε ( FObj F_T a )) o ( FMap F_T ( TMap nat-η a )) ] - ≈ id1 KleisliCategory (FObj F_T a) ] + ≈ id1 KleisliCategory (FObj F_T a) ] adjoint2 {a} = let open ≈-Reasoning (A) in begin KMap (( TMap nat-ε ( FObj F_T a )) * ( FMap F_T ( TMap nat-η a )) ) @@ -536,36 +539,33 @@ KMap (id1 KleisliCategory (FObj F_T a)) ∎ -nat-μ : NTrans A A (( U_T ○ F_T ) ○ (U_T ○ F_T)) (U_T ○ F_T) -nat-μ = {!!} +open MResolution -M_T : Monad A ( U_T ○ F_T ) nat-η nat-μ -M_T = {!!} - -Resolution_T : Resolution A KleisliCategory T M U_T F_T Adj_T +Resolution_T : MResolution A KleisliCategory T M U_T F_T Adj_T Resolution_T = record { - T=UF = {!!} ; - μ=UεF = {!!} + T=UF = Lemma11; + μ=UεF = Lemma12 } -module comparison-functor {c₁' c₂' ℓ' : Level} ( B : Category c₁ c₂ ℓ ) +module comparison-functor {c₁' c₂' ℓ' : Level} ( B : Category c₁' c₂' ℓ' ) { U_K : Functor B A } { F_K : Functor A B } { η_K : NTrans A A identityFunctor ( U_K ○ F_K ) } { ε_K : NTrans B B ( F_K ○ U_K ) identityFunctor } { μ_K : NTrans A A (( U_K ○ F_K ) ○ ( U_K ○ F_K )) ( U_K ○ F_K ) } - ( MK : Monad A (U_K ○ F_K) η_K μ_K ) + ( K : Monad A (U_K ○ F_K) η_K μ_K ) ( AdjK : Adjunction A B U_K F_K η_K ε_K ) - ( ResK : Resolution A B T M AdjK ) + (ResK : MResolution A B T M U_K F_K AdjK ) where - kfmap : {!!} - kfmap = {!!} + RHom = \(a b : Obj A) -> KleisliHom {c₁} {c₂} {ℓ} {A} { U_K ○ F_K } a b + kfmap : {a b : Obj A} (f : RHom a b) -> Hom B (FObj F_K a) (FObj F_K b) + kfmap {_} {b} f = B [ TMap ε_K (FObj F_K b) o FMap F_K (KMap f) ] K_T : Functor KleisliCategory B K_T = record { FObj = FObj F_K - ; FMap = kfmap + ; FMap = {!!} -- kfmap ; isFunctor = record { ≈-cong = {!!} -- ≈-cong ; identity = {!!} -- identity