Mercurial > hg > Members > kono > Proof > category

changeset 707:808b03184fd3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Applicative ⇔ Monoidal without commutative laws
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 22 Nov 2017 14:07:17 +0900
parents dad072d52d0e
children 975aa343a963
files monoidal.agda
diffstat 1 files changed, 5 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/monoidal.agda	Wed Nov 22 12:49:17 2017 +0900
+++ b/monoidal.agda	Wed Nov 22 14:07:17 2017 +0900
@@ -331,6 +331,7 @@
   field
       pure  : {a : Obj Sets} → Hom Sets a ( FObj f a )
       <*>   : {a b : Obj Sets} → FObj f ( a → b ) → FObj f a → FObj f b
+      --  should have Applicative law
 
 lemma1 : {c₁ : Level} ( f : Functor (Sets {c₁}) (Sets {c₁}) ) → Applicative f → HaskellMonoidalFunctor f
 lemma1 f app = record { unit = unit ; φ = φ }
@@ -339,13 +340,13 @@
      unit  :  FObj f One
      unit = pure app OneObj
      φ :  {a b : Obj Sets} → Hom Sets ((FObj f a) *  (FObj f b )) ( FObj f ( a * b ) )
-     φ {a} {b} ( x , y ) = <*> app {!!} {!!}
+     φ {a} {b} ( x , y ) = <*> app (FMap f (λ j k → (j , k)) x) y
 
 lemma2 : {c₁ : Level} ( f : Functor (Sets {c₁}) (Sets {c₁}) ) → HaskellMonoidalFunctor f → Applicative f 
-lemma2 f app = record { pure = pure ; <*> = <*> }
+lemma2 f mono = record { pure = pure ; <*> = <*> }
   where
      open HaskellMonoidalFunctor
      pure  :  {a : Obj Sets} → Hom Sets a ( FObj f a )
-     pure {a} x = {!!} -- (unit app)
+     pure {a} x = FMap f ( λ y → x ) (unit mono)
      <*> :   {a b : Obj Sets} → FObj f ( a → b ) → FObj f a → FObj f b
-     <*> {a} {b} x = {!!}
+     <*> {a} {b} x y = FMap f ( λ a→b*b →  ( proj₁ a→b*b )  ( proj₂  a→b*b ) )  ( ** mono  x y  )