Mercurial > hg > Members > kono > Proof > category
changeset 765:171f5386e87e
Applicative→HaskellMonoidal begin
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 12 Dec 2017 00:20:07 +0900 |
| parents | 01c618d94278 |
| children | c30ca91f3a76 |
| files | monoidal.agda |
| diffstat | 1 files changed, 34 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- a/monoidal.agda Mon Dec 11 23:43:52 2017 +0900 +++ b/monoidal.agda Tue Dec 12 00:20:07 2017 +0900 @@ -979,3 +979,37 @@ where open Relation.Binary.PropositionalEquality.≡-Reasoning +---- +-- +-- Applicative laws imples Monoidal laws +-- + +Applicative→HaskellMonoidal : {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) ) + ( pure : {a : Obj Sets} → Hom Sets a ( FObj F a ) ) + ( <*> : {a b : Obj Sets} → FObj F ( a → b ) → FObj F a → FObj F b ) + ( app : IsApplicative F pure <*> ) + → IsHaskellMonoidalFunctor F (pure OneObj) (λ x → <*> (FMap F (λ j k → (j , k)) ( proj₁ x)) ( proj₂ x) ) +Applicative→HaskellMonoidal {l} F pure <*> app = record { + natφ = natφ + ; assocφ = assocφ + ; idrφ = idrφ + ; idlφ = idlφ + } where + unit : FObj F One + unit = pure OneObj + φ : {a b : Obj Sets} → Hom Sets ((FObj F a) * (FObj F b )) ( FObj F ( a * b ) ) + φ = λ x → <*> (FMap F (λ j k → (j , k)) ( proj₁ x)) ( proj₂ x) + isM : IsMonoidal (Sets {l}) One SetsTensorProduct + isM = Monoidal.isMonoidal MonoidalSets + natφ : { a b c d : Obj Sets } { x : FObj F a} { y : FObj F b} { f : a → c } { g : b → d } + → FMap F (map f g) (φ (x , y)) ≡ φ (FMap F f x , FMap F g y) + natφ = {!!} + assocφ : { x y z : Obj Sets } { a : FObj F x } { b : FObj F y }{ c : FObj F z } + → φ (a , φ (b , c)) ≡ FMap F (Iso.≅→ (IsMonoidal.mα-iso isM)) (φ (φ (a , b) , c)) + assocφ = {!!} + idrφ : {a : Obj Sets } { x : FObj F a } → FMap F (Iso.≅→ (IsMonoidal.mρ-iso isM)) (φ (x , unit)) ≡ x + idrφ = {!!} + idlφ : {a : Obj Sets } { x : FObj F a } → FMap F (Iso.≅→ (IsMonoidal.mλ-iso isM)) (φ (unit , x)) ≡ x + idlφ = {!!} + +