Mercurial > hg > Members > kono > Proof > category
changeset 719:a017ed40dd77
Applicative law → Monoidal law begin
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 24 Nov 2017 16:38:34 +0900 |
| parents | f2e617dc2c21 |
| children | 13cef2bfa5c8 |
| files | monoidal.agda |
| diffstat | 1 files changed, 92 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- a/monoidal.agda Fri Nov 24 14:27:07 2017 +0900 +++ b/monoidal.agda Fri Nov 24 16:38:34 2017 +0900 @@ -519,6 +519,98 @@ <*> : {a b : Obj Sets} → FObj F ( a → b ) → FObj F a → FObj F b -- ** mono x y <*> {a} {b} x y = FMap F ( λ r → ( proj₁ r ) ( proj₂ r ) ) (φ mono ( x , y )) +Applicative→Monoidal : {c : Level} ( F : Functor (Sets {c}) (Sets {c}) ) → (mf : Applicative F ) + → IsApplicative F ( Applicative.pure mf ) ( Applicative.<*> mf ) + → MonoidalFunctor {_} {c} {_} {Sets} {Sets} MonoidalSets MonoidalSets +Applicative→Monoidal F mf ismf = record { + MF = F + ; ψ = λ x → unit + ; isMonodailFunctor = record { + φab = record { TMap = λ x → φ ; isNTrans = record { commute = comm0 } } + ; associativity = λ {a b c} → comm1 {a} {b} {c} + ; unitarity-idr = λ {a b} → comm2 {a} {b} + ; unitarity-idl = λ {a b} → comm3 {a} {b} + } + } where + open Monoidal + open IsMonoidal hiding ( _■_ ; _□_ ) + M = MonoidalSets + isM = Monoidal.isMonoidal MonoidalSets + unit = Applicative.pure mf OneObj + _⊗_ : (x y : Obj Sets ) → Obj Sets + _⊗_ x y = (IsMonoidal._□_ (Monoidal.isMonoidal M) ) x y + _□_ : {a b c d : Obj Sets } ( f : Hom Sets a c ) ( g : Hom Sets b d ) → Hom Sets ( a ⊗ b ) ( c ⊗ d ) + _□_ f g = FMap (m-bi M) ( f , g ) + φ : {x : Obj (Sets × Sets) } → Hom Sets (FObj (Functor● Sets Sets MonoidalSets F) x) (FObj (Functor⊗ Sets Sets MonoidalSets F) x) + φ x = Applicative.<*> mf (FMap F (λ j k → (j , k)) (proj₁ x )) (proj₂ x) + _<*>_ : {a b : Obj Sets} → FObj F ( a → b ) → FObj F a → FObj F b + _<*>_ = Applicative.<*> mf + comm00 : {a b : Obj (Sets × Sets)} { f : Hom (Sets × Sets) a b} (x : ( FObj F (proj₁ a) * FObj F (proj₂ a)) ) → + (Sets [ FMap (Functor⊗ Sets Sets MonoidalSets F) f o φ ]) x ≡ (Sets [ φ o FMap (Functor● Sets Sets MonoidalSets F) f ]) x + comm00 {a} {b} {(f , g)} (x , y) = begin + ( FMap (Functor⊗ Sets Sets MonoidalSets F) (f , g) ) ( φ (x , y) ) + ≡⟨⟩ + FMap F (λ xy → f (proj₁ xy) , g (proj₂ xy)) ((FMap F (λ j k → j , k) x) <*> y) + ≡⟨ {!!} ⟩ + (FMap F (λ j k → f j , k) x) <*> (FMap F g y) + ≡⟨ {!!} ⟩ + (FMap F (λ j k → j , k) (FMap F f x)) <*> (FMap F g y) + ≡⟨⟩ + φ ( ( FMap (Functor● Sets Sets MonoidalSets F) (f , g) ) ( x , y ) ) + ∎ + where + open Relation.Binary.PropositionalEquality.≡-Reasoning + comm0 : {a b : Obj (Sets × Sets)} { f : Hom (Sets × Sets) a b} → Sets [ Sets [ FMap (Functor⊗ Sets Sets MonoidalSets F) f o φ ] + ≈ Sets [ φ o FMap (Functor● Sets Sets MonoidalSets F) f ] ] + comm0 {a} {b} {f} = extensionality Sets ( λ (x : ( FObj F (proj₁ a) * FObj F (proj₂ a)) ) → comm00 x ) + comm10 : {a b c : Obj Sets} → (x : ((FObj F a ⊗ FObj F b) ⊗ FObj F c) ) → (Sets [ φ o Sets [ id1 Sets (FObj F a) □ φ o Iso.≅→ (mα-iso isM) ] ]) x ≡ + (Sets [ FMap F (Iso.≅→ (mα-iso isM)) o Sets [ φ o φ □ id1 Sets (FObj F c) ] ]) x + comm10 {x} {y} {f} ((a , b) , c ) = begin + {!!} + ≡⟨ {!!} ⟩ + {!!} + ∎ + where + open Relation.Binary.PropositionalEquality.≡-Reasoning + comm1 : {a b c : Obj Sets} → Sets [ Sets [ φ + o Sets [ (id1 Sets (FObj F a) □ φ ) o Iso.≅→ (mα-iso isM) ] ] + ≈ Sets [ FMap F (Iso.≅→ (mα-iso isM)) o Sets [ φ o (φ □ id1 Sets (FObj F c)) ] ] ] + comm1 {a} {b} {c} = extensionality Sets ( λ x → comm10 x ) + comm20 : {a b : Obj Sets} ( x : FObj F a * One ) → ( Sets [ + FMap F (Iso.≅→ (mρ-iso isM)) o Sets [ φ o + FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit )) ] ] ) x ≡ Iso.≅→ (mρ-iso isM) x + comm20 {a} {b} (x , OneObj ) = begin + (FMap F (Iso.≅→ (mρ-iso isM))) ( φ (( FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit))) (x , OneObj) )) + ≡⟨⟩ + FMap F proj₁ ((FMap F (λ j k → j , k) x) <*> (Applicative.pure mf OneObj)) + ≡⟨ ≡-cong ( λ k → FMap F proj₁ k) ( IsApplicative.interchange ismf ) ⟩ + FMap F proj₁ ((Applicative.pure mf (λ f → f OneObj)) <*> (FMap F (λ j k → j , k) x)) + ≡⟨ {!!} ⟩ + x + ≡⟨⟩ + Iso.≅→ (mρ-iso isM) (x , OneObj) + ∎ + where + open Relation.Binary.PropositionalEquality.≡-Reasoning + comm2 : {a b : Obj Sets} → Sets [ Sets [ + FMap F (Iso.≅→ (mρ-iso isM)) o Sets [ φ o + FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit )) ] ] ≈ Iso.≅→ (mρ-iso isM) ] + comm2 {a} {b} = extensionality Sets ( λ x → comm20 {a} {b} x ) + comm30 : {a b : Obj Sets} ( x : One * FObj F b ) → ( Sets [ + FMap F (Iso.≅→ (mλ-iso isM)) o Sets [ φ o + FMap (m-bi MonoidalSets) ((λ _ → unit ) , id1 Sets (FObj F b) ) ] ] ) x ≡ Iso.≅→ (mλ-iso isM) x + comm30 {a} {b} ( OneObj , x) = begin + {!!} + ≡⟨ {!!} ⟩ + {!!} + ∎ + where + open Relation.Binary.PropositionalEquality.≡-Reasoning + comm3 : {a b : Obj Sets} → Sets [ Sets [ FMap F (Iso.≅→ (mλ-iso isM)) o + Sets [ φ o FMap (m-bi MonoidalSets) ((λ _ → unit ) , id1 Sets (FObj F b)) ] ] ≈ Iso.≅→ (mλ-iso isM) ] + comm3 {a} {b} = extensionality Sets ( λ x → comm30 {a} {b} x ) + + HaskellMonoidal→Applicative : {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) ) ( unit : FObj F One )