Mercurial > hg > Members > kono > Proof > category
diff kleisli.agda @ 688:a5f2ca67e7c5
fix monad/adjunction definition
couniversal to limit does not work
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 11 Nov 2017 21:34:58 +0900 |
| parents | 2d32ded94aaf |
| children |
line wrap: on
line diff
--- a/kleisli.agda Wed Nov 08 19:57:43 2017 +0900 +++ b/kleisli.agda Sat Nov 11 21:34:58 2017 +0900 @@ -24,7 +24,7 @@ { T : Functor A A } { η : NTrans A A identityFunctor T } { μ : NTrans A A (T ○ T) T } - { M : Monad A T η μ } where + { M : IsMonad A T η μ } where --T(g f) = T(g) T(f) @@ -49,15 +49,14 @@ -- μ(a)(μ(T(a))) = μ(a)T(μ(a)) -- association law -open Monad Lemma3 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} { T : Functor A A } { η : NTrans A A identityFunctor T } { μ : NTrans A A (T ○ T) T } { a : Obj A } → - ( M : Monad A T η μ ) + ( M : IsMonad A T η μ ) → A [ A [ TMap μ a o TMap μ ( FObj T a ) ] ≈ A [ TMap μ a o FMap T (TMap μ a) ] ] -Lemma3 = λ m → IsMonad.assoc ( isMonad m ) +Lemma3 = λ m → IsMonad.assoc m Lemma4 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A } { f : Hom A a b} @@ -69,18 +68,18 @@ { η : NTrans A A identityFunctor T } { μ : NTrans A A (T ○ T) T } { a : Obj A } → - ( M : Monad A T η μ ) + ( M : IsMonad A T η μ ) → A [ A [ TMap μ a o TMap η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ] -Lemma5 = λ m → IsMonad.unity1 ( isMonad m ) +Lemma5 = λ m → IsMonad.unity1 m Lemma6 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} { T : Functor A A } { η : NTrans A A identityFunctor T } { μ : NTrans A A (T ○ T) T } { a : Obj A } → - ( M : Monad A T η μ ) + ( M : IsMonad A T η μ ) → A [ A [ TMap μ a o (FMap T (TMap η a )) ] ≈ Id {_} {_} {_} {A} (FObj T a) ] -Lemma6 = λ m → IsMonad.unity2 ( isMonad m ) +Lemma6 = λ m → IsMonad.unity2 m -- Laws of Kleisli Category -- @@ -91,6 +90,11 @@ -- h ○ (g ○ f) = (h ○ g) ○ f -- assocation law (Lemma9) -- η(b) ○ f = f + +join : (m : IsMonad A T η μ ) → { 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 ] ] + Lemma7 : { a : Obj A } { b : Obj A } ( f : Hom A a ( FObj T b) ) → A [ join M (TMap η b) f ≈ f ] Lemma7 {_} {b} f = @@ -101,7 +105,7 @@ A [ TMap μ b o A [ FMap T ((TMap η b)) o f ] ] ≈⟨ IsCategory.associative (Category.isCategory A) ⟩ A [ A [ TMap μ b o FMap T ((TMap η b)) ] o f ] - ≈⟨ car ( IsMonad.unity2 ( isMonad M) ) ⟩ + ≈⟨ car ( IsMonad.unity2 M ) ⟩ A [ id (FObj T b) o f ] ≈⟨ IsCategory.identityL (Category.isCategory A) ⟩ f @@ -120,7 +124,7 @@ A [ TMap μ b o A [ (TMap η ( FObj T b)) o f ] ] ≈⟨ IsCategory.associative (Category.isCategory A) ⟩ A [ A [ TMap μ b o (TMap η ( FObj T b)) ] o f ] - ≈⟨ car ( IsMonad.unity1 ( isMonad M) ) ⟩ + ≈⟨ car ( IsMonad.unity1 M ) ⟩ A [ id (FObj T b) o f ] ≈⟨ IsCategory.identityL (Category.isCategory A) ⟩ f @@ -170,7 +174,7 @@ ≈⟨ car ( car ( begin ( TMap μ d o TMap μ (FObj T d) ) - ≈⟨ IsMonad.assoc ( isMonad M) ⟩ + ≈⟨ IsMonad.assoc M ⟩ ( TMap μ d o FMap T (TMap μ d) ) ∎ )) ⟩ @@ -292,7 +296,7 @@ identity {a} = let open ≈-Reasoning (A) in begin TMap μ (a) o FMap T (TMap η a) - ≈⟨ IsMonad.unity2 (isMonad M) ⟩ + ≈⟨ IsMonad.unity2 M ⟩ id (FObj T a) ∎ ≈-cong : {a b : Obj A} {f g : KHom a b} → A [ KMap f ≈ KMap g ] → A [ ufmap f ≈ ufmap g ] @@ -314,7 +318,7 @@ TMap μ (c) o (( FMap T ( TMap μ (c)) o FMap T (FMap T (KMap g) o (KMap f)))) ≈⟨ assoc ⟩ (TMap μ (c) o ( FMap T ( TMap μ (c)))) o FMap T (FMap T (KMap g) o (KMap f)) - ≈⟨ car (sym (IsMonad.assoc (isMonad M))) ⟩ + ≈⟨ car (sym (IsMonad.assoc M)) ⟩ (TMap μ (c) o ( TMap μ (FObj T c))) o FMap T (FMap T (KMap g) o (KMap f)) ≈⟨ sym assoc ⟩ TMap μ (c) o (( TMap μ (FObj T c)) o FMap T (FMap T (KMap g) o (KMap f))) @@ -366,7 +370,7 @@ (FMap T g o TMap η (b)) o f ≈⟨ sym idL ⟩ id (FObj T c) o ((FMap T g o TMap η (b)) o f) - ≈⟨ sym (car (IsMonad.unity2 (isMonad M))) ⟩ + ≈⟨ sym (car (IsMonad.unity2 M)) ⟩ (TMap μ c o FMap T (TMap η c)) o ((FMap T g o TMap η (b)) o f) ≈⟨ sym assoc ⟩ TMap μ c o ( FMap T (TMap η c) o ((FMap T g o TMap η (b)) o f) ) @@ -408,7 +412,7 @@ TMap μ (b) o ( FMap T (TMap η (b)) o FMap T f) ≈⟨ assoc ⟩ (TMap μ (b) o FMap T (TMap η (b))) o FMap T f - ≈⟨ car (IsMonad.unity2 (isMonad M)) ⟩ + ≈⟨ car (IsMonad.unity2 M) ⟩ id (FObj T b) o FMap T f ≈⟨ idL ⟩ FMap T f @@ -464,7 +468,7 @@ TMap μ b o (TMap η (FObj T b) o (TMap μ (b) o FMap T (KMap f))) ≈⟨ assoc ⟩ (TMap μ b o (TMap η (FObj T b))) o (TMap μ (b) o FMap T (KMap f)) - ≈⟨ (car (IsMonad.unity1 (isMonad M))) ⟩ + ≈⟨ (car (IsMonad.unity1 M)) ⟩ id (FObj T b) o (TMap μ (b) o FMap T (KMap f)) ≈⟨ idL ⟩ TMap μ b o FMap T (KMap f) @@ -525,8 +529,12 @@ TMap μ x ∎ ) -Adj_T : Adjunction A KleisliCategory U_T F_T nat-η nat-ε +Adj_T : Adjunction A KleisliCategory Adj_T = record { + U = U_T ; + F = F_T ; + η = nat-η ; + ε = nat-ε ; isAdjunction = record { adjoint1 = adjoint1 ; adjoint2 = adjoint2 @@ -543,7 +551,7 @@ (TMap μ (b) o (id (FObj T (FObj T b )))) o ( TMap η ( FObj T b )) ≈⟨ car idR ⟩ TMap μ (b) o ( TMap η ( FObj T b )) - ≈⟨ IsMonad.unity1 (isMonad M) ⟩ + ≈⟨ IsMonad.unity1 M ⟩ id (FObj U_T b) ∎ adjoint2 : {a : Obj A} → @@ -560,7 +568,7 @@ TMap μ a o ((TMap η (FObj T a)) o (TMap η a)) ≈⟨ assoc ⟩ (TMap μ a o (TMap η (FObj T a))) o (TMap η a) - ≈⟨ car (IsMonad.unity1 (isMonad M)) ⟩ + ≈⟨ car (IsMonad.unity1 M) ⟩ id (FObj T a) o (TMap η a) ≈⟨ idL ⟩ TMap η a @@ -572,8 +580,14 @@ open MResolution -Resolution_T : MResolution A KleisliCategory T U_T F_T {nat-η} {nat-ε} {nat-μ} Adj_T +Resolution_T : MResolution A KleisliCategory ( record { T = T ; η = η ; μ = μ; isMonad = M } ) Resolution_T = record { + UR = U_T ; + FR = F_T ; + ηR = nat-η ; + εR = nat-ε ; + μR = nat-μ ; + Adj = Adjunction.isAdjunction Adj_T ; T=UF = Lemma11; μ=UεF = Lemma12 }