Mercurial > hg > Members > kono > Proof > category
annotate applicative.agda @ 790:1e7319868d77
Sets is CCC
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 19 Apr 2019 23:42:19 +0900 |
| parents | bded2347efa4 |
| children | dca4b29553cb |
| rev | line source |
|---|---|
|
696
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
1 open import Level |
|
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
2 open import Category |
| 768 | 3 module applicative where |
|
696
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
4 |
|
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
5 open import Data.Product renaming (_×_ to _*_) |
|
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
6 open import Category.Constructions.Product |
|
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
7 open import HomReasoning |
|
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
8 open import cat-utility |
|
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
9 open import Relation.Binary.Core |
|
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
10 open import Relation.Binary |
| 768 | 11 open import monoidal |
| 783 | 12 open import Relation.Binary.PropositionalEquality hiding ( [_] ) |
| 769 | 13 |
| 14 ----- | |
| 15 -- | |
| 16 -- Applicative Functor | |
| 17 -- | |
| 18 -- is a monoidal functor on Sets and it can be constructoed from Haskell monoidal functor and vais versa | |
| 19 -- | |
| 20 ---- | |
| 21 | |
| 22 ----- | |
| 23 -- | |
| 24 -- To show Applicative functor is monoidal functor, uniquness of Functor is necessary, which is derived from the free theorem. | |
| 25 -- | |
| 26 -- they say it is not possible to prove FreeTheorem in Agda nor Coq | |
| 27 -- https://stackoverflow.com/questions/24718567/is-it-possible-to-get-hold-of-free-theorems-as-propositional-equalities | |
| 28 -- so we postulate this | |
| 29 -- and we cannot indent a postulate ... | |
| 30 | |
| 31 open Functor | |
| 32 | |
| 33 postulate FreeTheorem : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (C : Category c₁ c₂ ℓ) (D : Category c₁' c₂' ℓ') {a b c : Obj C } → (F : Functor C D ) → ( fmap : {a : Obj C } {b : Obj C } → Hom C a b → Hom D (FObj F a) ( FObj F b) ) → {h f : Hom C a b } → {g k : Hom C b c } → C [ C [ g o h ] ≈ C [ k o f ] ] → D [ D [ FMap F g o fmap h ] ≈ D [ fmap k o FMap F f ] ] | |
| 34 | |
| 35 UniquenessOfFunctor : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (C : Category c₁ c₂ ℓ) (D : Category c₁' c₂' ℓ') (F : Functor C D) | |
| 36 {a b : Obj C } { f : Hom C a b } → ( fmap : {a : Obj C } {b : Obj C } → Hom C a b → Hom D (FObj F a) ( FObj F b) ) | |
| 37 → ( {b : Obj C } → D [ fmap (id1 C b) ≈ id1 D (FObj F b) ] ) | |
| 38 → D [ fmap f ≈ FMap F f ] | |
| 39 UniquenessOfFunctor C D F {a} {b} {f} fmap eq = begin | |
| 40 fmap f | |
| 41 ≈↑⟨ idL ⟩ | |
| 42 id1 D (FObj F b) o fmap f | |
| 43 ≈↑⟨ car ( IsFunctor.identity (isFunctor F )) ⟩ | |
| 44 FMap F (id1 C b) o fmap f | |
| 45 ≈⟨ FreeTheorem C D F fmap (IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory C ))) ⟩ | |
| 46 fmap (id1 C b) o FMap F f | |
| 47 ≈⟨ car eq ⟩ | |
| 48 id1 D (FObj F b) o FMap F f | |
| 49 ≈⟨ idL ⟩ | |
| 50 FMap F f | |
| 51 ∎ | |
| 52 where open ≈-Reasoning D | |
| 53 | |
| 768 | 54 open import Category.Sets |
| 55 import Relation.Binary.PropositionalEquality | |
|
696
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
56 |
|
705
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
57 |
| 720 | 58 _・_ : {c₁ : Level} { a b c : Obj (Sets {c₁} ) } → (b → c) → (a → b) → a → c |
| 59 _・_ f g = λ x → f ( g x ) | |
| 713 | 60 |
| 766 | 61 record IsApplicative {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) ) |
| 62 ( pure : {a : Obj Sets} → Hom Sets a ( FObj F a ) ) | |
| 63 ( _<*>_ : {a b : Obj Sets} → FObj F ( a → b ) → FObj F a → FObj F b ) | |
| 713 | 64 : Set (suc (suc c₁)) where |
| 65 field | |
| 766 | 66 identity : { a : Obj Sets } { u : FObj F a } → pure ( id1 Sets a ) <*> u ≡ u |
| 67 composition : { a b c : Obj Sets } { u : FObj F ( b → c ) } { v : FObj F (a → b ) } { w : FObj F a } | |
| 713 | 68 → (( pure _・_ <*> u ) <*> v ) <*> w ≡ u <*> (v <*> w) |
| 69 homomorphism : { a b : Obj Sets } { f : Hom Sets a b } { x : a } → pure f <*> pure x ≡ pure (f x) | |
| 766 | 70 interchange : { a b : Obj Sets } { u : FObj F ( a → b ) } { x : a } → u <*> pure x ≡ pure (λ f → f x) <*> u |
| 730 | 71 -- from http://www.staff.city.ac.uk/~ross/papers/Applicative.pdf |
| 713 | 72 |
| 73 record Applicative {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) ) | |
|
705
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
74 : Set (suc (suc c₁)) where |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
75 field |
| 713 | 76 pure : {a : Obj Sets} → Hom Sets a ( FObj F a ) |
| 77 <*> : {a b : Obj Sets} → FObj F ( a → b ) → FObj F a → FObj F b | |
| 766 | 78 isApplicative : IsApplicative F pure <*> |
| 713 | 79 |
| 730 | 80 ------ |
| 81 -- | |
| 82 -- Appllicative Functor is a Monoidal Functor | |
| 83 -- | |
| 84 | |
|
719
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
85 Applicative→Monoidal : {c : Level} ( F : Functor (Sets {c}) (Sets {c}) ) → (mf : Applicative F ) |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
86 → IsApplicative F ( Applicative.pure mf ) ( Applicative.<*> mf ) |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
87 → MonoidalFunctor {_} {c} {_} {Sets} {Sets} MonoidalSets MonoidalSets |
|
727
ea84cc6c1797
monoidal functor and applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
726
diff
changeset
|
88 Applicative→Monoidal {l} F mf ismf = record { |
|
719
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
89 MF = F |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
90 ; ψ = λ x → unit |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
91 ; isMonodailFunctor = record { |
| 769 | 92 φab = record { TMap = λ x → φ ; isNTrans = record { commute = φab-comm } } |
| 93 ; associativity = λ {a b c} → associativity {a} {b} {c} | |
| 94 ; unitarity-idr = λ {a b} → unitarity-idr {a} {b} | |
| 95 ; unitarity-idl = λ {a b} → unitarity-idl {a} {b} | |
|
719
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
96 } |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
97 } where |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
98 open Monoidal |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
99 open IsMonoidal hiding ( _■_ ; _□_ ) |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
100 M = MonoidalSets |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
101 isM = Monoidal.isMonoidal MonoidalSets |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
102 unit = Applicative.pure mf OneObj |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
103 _⊗_ : (x y : Obj Sets ) → Obj Sets |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
104 _⊗_ x y = (IsMonoidal._□_ (Monoidal.isMonoidal M) ) x y |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
105 _□_ : {a b c d : Obj Sets } ( f : Hom Sets a c ) ( g : Hom Sets b d ) → Hom Sets ( a ⊗ b ) ( c ⊗ d ) |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
106 _□_ f g = FMap (m-bi M) ( f , g ) |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
107 φ : {x : Obj (Sets × Sets) } → Hom Sets (FObj (Functor● Sets Sets MonoidalSets F) x) (FObj (Functor⊗ Sets Sets MonoidalSets F) x) |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
108 φ x = Applicative.<*> mf (FMap F (λ j k → (j , k)) (proj₁ x )) (proj₂ x) |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
109 _<*>_ : {a b : Obj Sets} → FObj F ( a → b ) → FObj F a → FObj F b |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
110 _<*>_ = Applicative.<*> mf |
|
721
a8b595fb4905
use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
111 left : {a b : Obj Sets} → {x y : FObj F ( a → b )} → {h : FObj F a } → ( x ≡ y ) → x <*> h ≡ y <*> h |
|
a8b595fb4905
use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
112 left {_} {_} {_} {_} {h} eq = ≡-cong ( λ k → k <*> h ) eq |
|
a8b595fb4905
use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
113 right : {a b : Obj Sets} → {h : FObj F ( a → b )} → {x y : FObj F a } → ( x ≡ y ) → h <*> x ≡ h <*> y |
|
a8b595fb4905
use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
114 right {_} {_} {h} {_} {_} eq = ≡-cong ( λ k → h <*> k ) eq |
|
a8b595fb4905
use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
115 id : { a : Obj Sets } → a → a |
|
a8b595fb4905
use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
116 id x = x |
| 720 | 117 pure : {a : Obj Sets } → Hom Sets a ( FObj F a ) |
| 118 pure a = Applicative.pure mf a | |
| 725 | 119 -- special case |
| 120 F→pureid : {a b : Obj Sets } → (x : FObj F a ) → FMap F id x ≡ pure id <*> x | |
| 121 F→pureid {a} {b} x = sym ( begin | |
|
722
69f01b82dfc9
uniquness of functor fmap
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
721
diff
changeset
|
122 pure id <*> x |
|
69f01b82dfc9
uniquness of functor fmap
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
721
diff
changeset
|
123 ≡⟨ IsApplicative.identity ismf ⟩ |
|
69f01b82dfc9
uniquness of functor fmap
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
721
diff
changeset
|
124 x |
|
69f01b82dfc9
uniquness of functor fmap
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
721
diff
changeset
|
125 ≡⟨ ≡-cong ( λ k → k x ) (sym ( IsFunctor.identity (isFunctor F ) )) ⟩ FMap F id x |
|
69f01b82dfc9
uniquness of functor fmap
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
721
diff
changeset
|
126 ∎ ) |
|
69f01b82dfc9
uniquness of functor fmap
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
721
diff
changeset
|
127 where |
|
69f01b82dfc9
uniquness of functor fmap
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
721
diff
changeset
|
128 open Relation.Binary.PropositionalEquality |
|
69f01b82dfc9
uniquness of functor fmap
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
721
diff
changeset
|
129 open Relation.Binary.PropositionalEquality.≡-Reasoning |
| 725 | 130 F→pure : {a b : Obj Sets } → { f : a → b } → {x : FObj F a } → FMap F f x ≡ pure f <*> x |
| 131 F→pure {a} {b} {f} {x} = sym ( begin | |
|
721
a8b595fb4905
use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
132 pure f <*> x |
|
731
117e5b392673
Generalize Free Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
730
diff
changeset
|
133 ≡⟨ ≡-cong ( λ k → k x ) (UniquenessOfFunctor Sets Sets F ( λ f x → pure f <*> x ) ( extensionality Sets ( λ x → IsApplicative.identity ismf ))) ⟩ |
|
721
a8b595fb4905
use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
134 FMap F f x |
|
a8b595fb4905
use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
135 ∎ ) |
|
a8b595fb4905
use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
136 where |
|
a8b595fb4905
use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
137 open Relation.Binary.PropositionalEquality |
|
a8b595fb4905
use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
138 open Relation.Binary.PropositionalEquality.≡-Reasoning |
| 725 | 139 p*p : { a b : Obj Sets } { f : Hom Sets a b } { x : a } → pure f <*> pure x ≡ pure (f x) |
| 140 p*p = IsApplicative.homomorphism ismf | |
| 141 comp = IsApplicative.composition ismf | |
| 142 inter = IsApplicative.interchange ismf | |
| 729 | 143 pureAssoc : {a b c : Obj Sets } ( f : b → c ) ( g : a → b ) ( h : FObj F a ) → pure f <*> ( pure g <*> h ) ≡ pure ( f ・ g ) <*> h |
| 144 pureAssoc f g h = trans ( trans (sym comp) (left (left p*p) )) ( left p*p ) | |
| 145 where | |
| 146 open Relation.Binary.PropositionalEquality | |
| 769 | 147 φab-comm0 : {a b : Obj (Sets × Sets)} { f : Hom (Sets × Sets) a b} (x : ( FObj F (proj₁ a) * FObj F (proj₂ a)) ) → |
|
719
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
148 (Sets [ FMap (Functor⊗ Sets Sets MonoidalSets F) f o φ ]) x ≡ (Sets [ φ o FMap (Functor● Sets Sets MonoidalSets F) f ]) x |
| 769 | 149 φab-comm0 {a} {b} {(f , g)} (x , y) = begin |
|
719
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
150 ( FMap (Functor⊗ Sets Sets MonoidalSets F) (f , g) ) ( φ (x , y) ) |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
151 ≡⟨⟩ |
| 725 | 152 FMap F (λ xy → f (proj₁ xy) , g (proj₂ xy)) ((FMap F (λ j k → j , k) x) <*> y) |
| 153 ≡⟨⟩ | |
|
721
a8b595fb4905
use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
154 FMap F (map f g) ((FMap F (λ j k → j , k) x) <*> y) |
| 725 | 155 ≡⟨ F→pure ⟩ |
| 156 (pure (map f g) <*> (FMap F (λ j k → j , k) x <*> y)) | |
| 157 ≡⟨ right ( left F→pure ) ⟩ | |
|
721
a8b595fb4905
use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
158 (pure (map f g)) <*> ((pure (λ j k → j , k) <*> x) <*> y) |
|
a8b595fb4905
use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
159 ≡⟨ sym ( IsApplicative.composition ismf ) ⟩ |
|
a8b595fb4905
use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
160 (( pure _・_ <*> (pure (map f g))) <*> (pure (λ j k → j , k) <*> x)) <*> y |
|
a8b595fb4905
use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
161 ≡⟨ left ( sym ( IsApplicative.composition ismf )) ⟩ |
|
a8b595fb4905
use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
162 ((( pure _・_ <*> (( pure _・_ <*> (pure (map f g))))) <*> pure (λ j k → j , k)) <*> x) <*> y |
| 725 | 163 ≡⟨ trans ( trans (left ( left (left (right p*p )))) ( left ( left ( left p*p)))) (left (left p*p)) ⟩ |
|
721
a8b595fb4905
use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
164 (pure (( _・_ (( _・_ ((map f g))))) (λ j k → j , k)) <*> x) <*> y |
|
a8b595fb4905
use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
165 ≡⟨⟩ |
|
a8b595fb4905
use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
166 (pure (λ j k → f j , g k) <*> x) <*> y |
| 725 | 167 ≡⟨⟩ |
|
721
a8b595fb4905
use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
168 ( pure ((_・_ (( _・_ ( ( λ h → h g ))) ( _・_ ))) ((λ j k → f j , k))) <*> x ) <*> y |
| 725 | 169 ≡⟨ sym ( trans (left (left (left p*p))) (left ( left p*p)) ) ⟩ |
| 170 ((((pure _・_ <*> pure ((λ h → h g) ・ _・_)) <*> pure (λ j k → f j , k)) <*> x) <*> y) | |
| 171 ≡⟨ sym (trans ( left ( left ( left (right (left p*p) )))) (left ( left (left (right p*p ))))) ⟩ | |
|
721
a8b595fb4905
use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
172 (((pure _・_ <*> (( pure _・_ <*> ( pure ( λ h → h g ))) <*> ( pure _・_ ))) <*> (pure (λ j k → f j , k))) <*> x ) <*> y |
|
a8b595fb4905
use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
173 ≡⟨ left ( ( IsApplicative.composition ismf )) ⟩ |
|
a8b595fb4905
use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
174 ((( pure _・_ <*> ( pure ( λ h → h g ))) <*> ( pure _・_ )) <*> (pure (λ j k → f j , k) <*> x )) <*> y |
|
a8b595fb4905
use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
175 ≡⟨ left (IsApplicative.composition ismf ) ⟩ |
|
a8b595fb4905
use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
176 ( pure ( λ h → h g ) <*> ( pure _・_ <*> (pure (λ j k → f j , k) <*> x )) ) <*> y |
|
a8b595fb4905
use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
177 ≡⟨ left (sym (IsApplicative.interchange ismf )) ⟩ |
|
a8b595fb4905
use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
178 (( pure _・_ <*> (pure (λ j k → f j , k) <*> x )) <*> pure g) <*> y |
|
a8b595fb4905
use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
179 ≡⟨ IsApplicative.composition ismf ⟩ |
|
a8b595fb4905
use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
180 (pure (λ j k → f j , k) <*> x) <*> (pure g <*> y) |
| 725 | 181 ≡⟨ sym ( trans (left F→pure ) ( right F→pure ) ) ⟩ |
|
719
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
182 (FMap F (λ j k → f j , k) x) <*> (FMap F g y) |
| 720 | 183 ≡⟨ ≡-cong ( λ k → k x <*> (FMap F g y)) ( IsFunctor.distr (isFunctor F )) ⟩ |
|
719
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
184 (FMap F (λ j k → j , k) (FMap F f x)) <*> (FMap F g y) |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
185 ≡⟨⟩ |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
186 φ ( ( FMap (Functor● Sets Sets MonoidalSets F) (f , g) ) ( x , y ) ) |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
187 ∎ |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
188 where |
|
721
a8b595fb4905
use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
189 open Relation.Binary.PropositionalEquality |
|
719
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
190 open Relation.Binary.PropositionalEquality.≡-Reasoning |
| 769 | 191 φab-comm : {a b : Obj (Sets × Sets)} { f : Hom (Sets × Sets) a b} → Sets [ Sets [ FMap (Functor⊗ Sets Sets MonoidalSets F) f o φ ] |
|
719
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
192 ≈ Sets [ φ o FMap (Functor● Sets Sets MonoidalSets F) f ] ] |
| 769 | 193 φab-comm {a} {b} {f} = extensionality Sets ( λ (x : ( FObj F (proj₁ a) * FObj F (proj₂ a)) ) → φab-comm0 x ) |
| 194 associativity0 : {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 ≡ | |
|
719
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
195 (Sets [ FMap F (Iso.≅→ (mα-iso isM)) o Sets [ φ o φ □ id1 Sets (FObj F c) ] ]) x |
| 769 | 196 associativity0 {x} {y} {f} ((a , b) , c ) = begin |
|
721
a8b595fb4905
use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
197 φ (( id □ φ ) ( ( Iso.≅→ (mα-iso isM) ) ((a , b) , c))) |
| 720 | 198 ≡⟨⟩ |
| 199 (FMap F (λ j k → j , k) a) <*> ( (FMap F (λ j k → j , k) b) <*> c) | |
| 726 | 200 ≡⟨ trans (left F→pure) (right (left F→pure) ) ⟩ |
| 725 | 201 (pure (λ j k → j , k) <*> a) <*> ( (pure (λ j k → j , k) <*> b) <*> c) |
| 726 | 202 ≡⟨ sym comp ⟩ |
| 725 | 203 ( ( pure _・_ <*> (pure (λ j k → j , k) <*> a)) <*> (pure (λ j k → j , k) <*> b)) <*> c |
| 726 | 204 ≡⟨ sym ( left comp ) ⟩ |
| 725 | 205 (( ( pure _・_ <*> ( pure _・_ <*> (pure (λ j k → j , k) <*> a))) <*> (pure (λ j k → j , k))) <*> b) <*> c |
| 726 | 206 ≡⟨ sym ( left ( left ( left (right comp )))) ⟩ |
| 725 | 207 (( ( pure _・_ <*> (( (pure _・_ <*> pure _・_ ) <*> (pure (λ j k → j , k))) <*> a)) <*> (pure (λ j k → j , k))) <*> b) <*> c |
| 726 | 208 ≡⟨ trans (left ( left (left ( right (left ( left p*p )))))) (left ( left ( left (right (left p*p))))) ⟩ |
| 725 | 209 (( ( pure _・_ <*> ((pure ((_・_ ( _・_ )) ((λ j k → j , k)))) <*> a)) <*> (pure (λ j k → j , k))) <*> b) <*> c |
| 726 | 210 ≡⟨ sym (left ( left ( left comp ) )) ⟩ |
| 725 | 211 (((( ( pure _・_ <*> (pure _・_ )) <*> (pure ((_・_ ( _・_ )) ((λ j k → j , k))))) <*> a) <*> (pure (λ j k → j , k))) <*> b) <*> c |
| 726 | 212 ≡⟨ trans (left ( left ( left (left (left p*p))))) (left ( left ( left (left p*p )))) ⟩ |
| 725 | 213 ((((pure ( ( _・_ (_・_ )) (((_・_ ( _・_ )) ((λ j k → j , k)))))) <*> a) <*> (pure (λ j k → j , k))) <*> b) <*> c |
| 214 ≡⟨⟩ | |
| 215 ((((pure (λ f g x y → f , g x y)) <*> a) <*> (pure (λ j k → j , k))) <*> b) <*> c | |
| 726 | 216 ≡⟨ left ( left inter ) ⟩ |
| 725 | 217 (((pure (λ f → f (λ j k → j , k))) <*> ((pure (λ f g x y → f , g x y)) <*> a) ) <*> b) <*> c |
| 726 | 218 ≡⟨ sym ( left ( left comp )) ⟩ |
| 725 | 219 (((( pure _・_ <*> (pure (λ f → f (λ j k → j , k)))) <*> (pure (λ f g x y → f , g x y))) <*> a ) <*> b) <*> c |
| 726 | 220 ≡⟨ trans (left ( left (left (left p*p) ))) (left (left (left p*p ) )) ⟩ |
| 725 | 221 (((pure (λ f g h → f , g , h)) <*> a) <*> b) <*> c |
| 726 | 222 ≡⟨ sym (trans ( left ( left ( left (left (right (right p*p))) ) )) (trans (left (left( left (left (right p*p))))) |
| 223 (trans (left (left (left (left p*p)))) (trans ( left (left (left (right (left (right p*p )))))) | |
| 224 (trans (left (left (left (right (left p*p))))) (trans (left (left (left (right p*p)))) (left (left (left p*p)))) ) ) ) | |
| 225 ) ) ⟩ | |
| 725 | 226 ((((pure _・_ <*> ((pure _・_ <*> ((pure _・_ <*> ( pure (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc))))))) <*> |
| 227 (( pure _・_ <*> ( pure _・_ <*> (pure (λ j k → j , k)))) <*> pure (λ j k → j , k))) <*> a) <*> b) <*> c | |
| 726 | 228 ≡⟨ left (left comp ) ⟩ |
| 725 | 229 (((pure _・_ <*> ((pure _・_ <*> ( pure (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc))))) <*> |
| 230 ((( pure _・_ <*> ( pure _・_ <*> (pure (λ j k → j , k)))) <*> pure (λ j k → j , k)) <*> a)) <*> b) <*> c | |
| 726 | 231 ≡⟨ left comp ⟩ |
| 725 | 232 ((pure _・_ <*> ( pure (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc))) <*> |
| 233 (((( pure _・_ <*> ( pure _・_ <*> (pure (λ j k → j , k)))) <*> pure (λ j k → j , k)) <*> a) <*> b)) <*> c | |
| 726 | 234 ≡⟨ left ( right (left comp )) ⟩ |
| 725 | 235 ((pure _・_ <*> ( pure (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc))) <*> |
| 236 ((( pure _・_ <*> (pure (λ j k → j , k))) <*> (pure (λ j k → j , k) <*> a)) <*> b)) <*> c | |
| 726 | 237 ≡⟨ left ( right comp ) ⟩ |
| 725 | 238 ((pure _・_ <*> ( pure (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc))) <*> |
| 239 (pure (λ j k → j , k) <*> ( (pure (λ j k → j , k) <*> a) <*> b))) <*> c | |
| 726 | 240 ≡⟨ comp ⟩ |
| 725 | 241 pure (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc) <*> ( (pure (λ j k → j , k) <*> ( (pure (λ j k → j , k) <*> a) <*> b)) <*> c) |
| 726 | 242 ≡⟨ sym ( trans ( trans F→pure (right (left F→pure ))) ( right ( left (right (left F→pure ))))) ⟩ |
| 720 | 243 FMap F (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc) ( (FMap F (λ j k → j , k) ( (FMap F (λ j k → j , k) a) <*> b)) <*> c) |
| 244 ≡⟨⟩ | |
| 245 ( FMap F (Iso.≅→ (mα-iso isM))) (φ (( φ □ id1 Sets (FObj F f) ) ((a , b) , c))) | |
|
719
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
246 ∎ |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
247 where |
| 720 | 248 open Relation.Binary.PropositionalEquality |
|
719
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
249 open Relation.Binary.PropositionalEquality.≡-Reasoning |
| 769 | 250 associativity : {a b c : Obj Sets} → Sets [ Sets [ φ |
|
719
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
251 o Sets [ (id1 Sets (FObj F a) □ φ ) o Iso.≅→ (mα-iso isM) ] ] |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
252 ≈ Sets [ FMap F (Iso.≅→ (mα-iso isM)) o Sets [ φ o (φ □ id1 Sets (FObj F c)) ] ] ] |
| 769 | 253 associativity {a} {b} {c} = extensionality Sets ( λ x → associativity0 x ) |
| 254 unitarity-idr0 : {a b : Obj Sets} ( x : FObj F a * One ) → ( Sets [ | |
|
719
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
255 FMap F (Iso.≅→ (mρ-iso isM)) o Sets [ φ o |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
256 FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit )) ] ] ) x ≡ Iso.≅→ (mρ-iso isM) x |
| 769 | 257 unitarity-idr0 {a} {b} (x , OneObj ) = begin |
|
719
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
258 (FMap F (Iso.≅→ (mρ-iso isM))) ( φ (( FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit))) (x , OneObj) )) |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
259 ≡⟨⟩ |
| 720 | 260 FMap F proj₁ ((FMap F (λ j k → j , k) x) <*> (pure OneObj)) |
|
719
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
261 ≡⟨ ≡-cong ( λ k → FMap F proj₁ k) ( IsApplicative.interchange ismf ) ⟩ |
| 720 | 262 FMap F proj₁ ((pure (λ f → f OneObj)) <*> (FMap F (λ j k → j , k) x)) |
| 725 | 263 ≡⟨ ( trans F→pure (right ( right F→pure )) ) ⟩ |
| 264 pure proj₁ <*> ((pure (λ f → f OneObj)) <*> (pure (λ j k → j , k) <*> x)) | |
| 265 ≡⟨ sym ( right comp ) ⟩ | |
| 266 pure proj₁ <*> (((pure _・_ <*> (pure (λ f → f OneObj))) <*> pure (λ j k → j , k)) <*> x) | |
| 267 ≡⟨ sym comp ⟩ | |
| 268 ( ( pure _・_ <*> (pure proj₁ ) ) <*> ((pure _・_ <*> (pure (λ f → f OneObj))) <*> pure (λ j k → j , k))) <*> x | |
| 269 ≡⟨ trans ( trans ( trans ( left ( left p*p)) ( left ( right (left p*p) ))) (left (right p*p) ) ) (left p*p) ⟩ | |
|
727
ea84cc6c1797
monoidal functor and applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
726
diff
changeset
|
270 pure ( ( _・_ (proj₁ {l} {l})) ((_・_ ((λ f → f OneObj))) (λ j k → j , k))) <*> x |
| 725 | 271 ≡⟨⟩ |
| 272 pure id <*> x | |
| 273 ≡⟨ IsApplicative.identity ismf ⟩ | |
|
719
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
274 x |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
275 ≡⟨⟩ |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
276 Iso.≅→ (mρ-iso isM) (x , OneObj) |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
277 ∎ |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
278 where |
| 725 | 279 open Relation.Binary.PropositionalEquality |
|
719
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
280 open Relation.Binary.PropositionalEquality.≡-Reasoning |
| 769 | 281 unitarity-idr : {a b : Obj Sets} → Sets [ Sets [ |
|
719
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
282 FMap F (Iso.≅→ (mρ-iso isM)) o Sets [ φ o |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
283 FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit )) ] ] ≈ Iso.≅→ (mρ-iso isM) ] |
| 769 | 284 unitarity-idr {a} {b} = extensionality Sets ( λ x → unitarity-idr0 {a} {b} x ) |
| 285 unitarity-idl0 : {a b : Obj Sets} ( x : One * FObj F b ) → ( Sets [ | |
|
719
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
286 FMap F (Iso.≅→ (mλ-iso isM)) o Sets [ φ o |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
287 FMap (m-bi MonoidalSets) ((λ _ → unit ) , id1 Sets (FObj F b) ) ] ] ) x ≡ Iso.≅→ (mλ-iso isM) x |
| 769 | 288 unitarity-idl0 {a} {b} ( OneObj , x) = begin |
| 720 | 289 (FMap F (Iso.≅→ (mλ-iso isM))) ( φ ( unit , x ) ) |
| 290 ≡⟨⟩ | |
| 291 FMap F proj₂ ((FMap F (λ j k → j , k) (pure OneObj)) <*> x) | |
| 725 | 292 ≡⟨ ( trans F→pure (right ( left F→pure )) ) ⟩ |
| 293 pure proj₂ <*> ((pure (λ j k → j , k) <*> (pure OneObj)) <*> x) | |
| 294 ≡⟨ sym comp ⟩ | |
| 295 ((pure _・_ <*> (pure proj₂)) <*> (pure (λ j k → j , k) <*> (pure OneObj))) <*> x | |
| 296 ≡⟨ trans (trans (left (left p*p )) (left ( right p*p)) ) (left p*p) ⟩ | |
|
727
ea84cc6c1797
monoidal functor and applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
726
diff
changeset
|
297 pure ((_・_ (proj₂ {l}) )((λ (j : One {l}) (k : b ) → j , k) OneObj)) <*> x |
| 725 | 298 ≡⟨⟩ |
| 299 pure id <*> x | |
| 300 ≡⟨ IsApplicative.identity ismf ⟩ | |
| 720 | 301 x |
| 302 ≡⟨⟩ | |
| 303 Iso.≅→ (mλ-iso isM) ( OneObj , x ) | |
|
719
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
304 ∎ |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
305 where |
| 725 | 306 open Relation.Binary.PropositionalEquality |
|
719
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
307 open Relation.Binary.PropositionalEquality.≡-Reasoning |
| 769 | 308 unitarity-idl : {a b : Obj Sets} → Sets [ Sets [ FMap F (Iso.≅→ (mλ-iso isM)) o |
|
719
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
309 Sets [ φ o FMap (m-bi MonoidalSets) ((λ _ → unit ) , id1 Sets (FObj F b)) ] ] ≈ Iso.≅→ (mλ-iso isM) ] |
| 769 | 310 unitarity-idl {a} {b} = extensionality Sets ( λ x → unitarity-idl0 {a} {b} x ) |
|
719
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
311 |
| 730 | 312 ---- |
| 313 -- | |
| 773 | 314 -- Monoidal laws implies Applicative laws |
| 730 | 315 -- |
| 713 | 316 |
| 317 HaskellMonoidal→Applicative : {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) ) | |
| 766 | 318 ( Mono : HaskellMonoidalFunctor F ) |
| 319 → Applicative F | |
| 320 HaskellMonoidal→Applicative {c₁} F Mono = record { | |
| 321 pure = pure ; | |
| 322 <*> = _<*>_ ; | |
| 323 isApplicative = record { | |
| 713 | 324 identity = identity |
| 325 ; composition = composition | |
| 326 ; homomorphism = homomorphism | |
| 327 ; interchange = interchange | |
| 328 } | |
| 766 | 329 } |
| 713 | 330 where |
| 766 | 331 unit : FObj F One |
| 332 unit = HaskellMonoidalFunctor.unit Mono | |
| 333 φ : {a b : Obj Sets} → Hom Sets ((FObj F a) * (FObj F b )) ( FObj F ( a * b ) ) | |
| 334 φ = HaskellMonoidalFunctor.φ Mono | |
| 335 mono : IsHaskellMonoidalFunctor F unit φ | |
| 336 mono = HaskellMonoidalFunctor.isHaskellMonoidalFunctor Mono | |
| 714 | 337 id : { a : Obj Sets } → a → a |
| 338 id x = x | |
| 713 | 339 isM : IsMonoidal (Sets {c₁}) One SetsTensorProduct |
| 340 isM = Monoidal.isMonoidal MonoidalSets | |
| 341 pure : {a : Obj Sets} → Hom Sets a ( FObj F a ) | |
| 342 pure {a} x = FMap F ( λ y → x ) (unit ) | |
| 343 _<*>_ : {a b : Obj Sets} → FObj F ( a → b ) → FObj F a → FObj F b | |
| 715 | 344 _<*>_ {a} {b} x y = FMap F ( λ r → ( proj₁ r ) ( proj₂ r ) ) (φ ( x , y )) |
|
721
a8b595fb4905
use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
345 -- right does not work right it makes yellows. why? |
|
a8b595fb4905
use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
346 -- right : {n : Level} { a b : Set n} → { x y : a } { h : a → b } → ( x ≡ y ) → h x ≡ h y |
|
a8b595fb4905
use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
347 -- right {_} {_} {_} {_} {_} {h} eq = ≡-cong ( λ k → h k ) eq |
|
a8b595fb4905
use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
348 left : {n : Level} { a b : Set n} → { x y : a → b } { h : a } → ( x ≡ y ) → x h ≡ y h |
|
a8b595fb4905
use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
349 left {_} {_} {_} {_} {_} {h} eq = ≡-cong ( λ k → k h ) eq |
| 715 | 350 open Relation.Binary.PropositionalEquality |
|
717
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
351 FφF→F : { a b c d e : Obj Sets } { g : Hom Sets a c } { h : Hom Sets b d } |
| 715 | 352 { f : Hom Sets (c * d) e } |
| 353 { x : FObj F a } { y : FObj F b } | |
| 354 → FMap F f ( φ ( FMap F g x , FMap F h y ) ) ≡ FMap F ( f o map g h ) ( φ ( x , y ) ) | |
|
717
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
355 FφF→F {a} {b} {c} {d} {e} {g} {h} {f} {x} {y} = sym ( begin |
| 715 | 356 FMap F ( f o map g h ) ( φ ( x , y ) ) |
| 357 ≡⟨ ≡-cong ( λ k → k ( φ ( x , y ))) ( IsFunctor.distr (isFunctor F) ) ⟩ | |
| 358 FMap F f (( FMap F ( map g h ) ) ( φ ( x , y ))) | |
| 359 ≡⟨ ≡-cong ( λ k → FMap F f k ) ( IsHaskellMonoidalFunctor.natφ mono ) ⟩ | |
| 360 FMap F f ( φ ( FMap F g x , FMap F h y ) ) | |
| 361 ∎ ) | |
| 362 where | |
| 363 open Relation.Binary.PropositionalEquality.≡-Reasoning | |
| 716 | 364 u→F : {a : Obj Sets } {u : FObj F a} → u ≡ FMap F id u |
| 365 u→F {a} {u} = sym ( ≡-cong ( λ k → k u ) ( IsFunctor.identity ( isFunctor F ) ) ) | |
| 366 φunitr : {a : Obj Sets } {u : FObj F a} → φ ( unit , u) ≡ FMap F (Iso.≅← (IsMonoidal.mλ-iso isM)) u | |
| 367 φunitr {a} {u} = sym ( begin | |
| 368 FMap F (Iso.≅← (IsMonoidal.mλ-iso isM)) u | |
| 369 ≡⟨ ≡-cong ( λ k → FMap F (Iso.≅← (IsMonoidal.mλ-iso isM)) k ) (sym (IsHaskellMonoidalFunctor.idlφ mono)) ⟩ | |
| 370 FMap F (Iso.≅← (IsMonoidal.mλ-iso isM)) ( FMap F (Iso.≅→ (IsMonoidal.mλ-iso isM)) ( φ ( unit , u) ) ) | |
|
721
a8b595fb4905
use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
371 ≡⟨ left ( sym ( IsFunctor.distr ( isFunctor F ) )) ⟩ |
| 716 | 372 (FMap F ( (Iso.≅← (IsMonoidal.mλ-iso isM)) o (Iso.≅→ (IsMonoidal.mλ-iso isM)))) ( φ ( unit , u) ) |
| 373 ≡⟨ ≡-cong ( λ k → FMap F k ( φ ( unit , u) )) (Iso.iso→ ( (IsMonoidal.mλ-iso isM) )) ⟩ | |
| 374 FMap F id ( φ ( unit , u) ) | |
|
721
a8b595fb4905
use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
375 ≡⟨ left ( IsFunctor.identity ( isFunctor F ) ) ⟩ |
| 716 | 376 id ( φ ( unit , u) ) |
| 377 ≡⟨⟩ | |
| 378 φ ( unit , u) | |
| 379 ∎ ) | |
| 380 where | |
| 381 open Relation.Binary.PropositionalEquality.≡-Reasoning | |
| 382 φunitl : {a : Obj Sets } {u : FObj F a} → φ ( u , unit ) ≡ FMap F (Iso.≅← (IsMonoidal.mρ-iso isM)) u | |
| 383 φunitl {a} {u} = sym ( begin | |
| 384 FMap F (Iso.≅← (IsMonoidal.mρ-iso isM)) u | |
| 385 ≡⟨ ≡-cong ( λ k → FMap F (Iso.≅← (IsMonoidal.mρ-iso isM)) k ) (sym (IsHaskellMonoidalFunctor.idrφ mono)) ⟩ | |
| 386 FMap F (Iso.≅← (IsMonoidal.mρ-iso isM)) ( FMap F (Iso.≅→ (IsMonoidal.mρ-iso isM)) ( φ ( u , unit ) ) ) | |
|
721
a8b595fb4905
use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
387 ≡⟨ left ( sym ( IsFunctor.distr ( isFunctor F ) )) ⟩ |
| 716 | 388 (FMap F ( (Iso.≅← (IsMonoidal.mρ-iso isM)) o (Iso.≅→ (IsMonoidal.mρ-iso isM)))) ( φ ( u , unit ) ) |
| 389 ≡⟨ ≡-cong ( λ k → FMap F k ( φ ( u , unit ) )) (Iso.iso→ ( (IsMonoidal.mρ-iso isM) )) ⟩ | |
| 390 FMap F id ( φ ( u , unit ) ) | |
|
721
a8b595fb4905
use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
391 ≡⟨ left ( IsFunctor.identity ( isFunctor F ) ) ⟩ |
| 716 | 392 id ( φ ( u , unit ) ) |
| 393 ≡⟨⟩ | |
| 394 φ ( u , unit ) | |
| 395 ∎ ) | |
| 396 where | |
| 397 open Relation.Binary.PropositionalEquality.≡-Reasoning | |
| 715 | 398 open IsMonoidal |
| 713 | 399 identity : { a : Obj Sets } { u : FObj F a } → pure ( id1 Sets a ) <*> u ≡ u |
| 400 identity {a} {u} = begin | |
| 714 | 401 pure id <*> u |
| 713 | 402 ≡⟨⟩ |
| 715 | 403 ( FMap F ( λ r → ( proj₁ r ) ( proj₂ r )) ) ( φ ( FMap F ( λ y → id ) unit , u ) ) |
| 716 | 404 ≡⟨ ≡-cong ( λ k → ( FMap F ( λ r → ( proj₁ r ) ( proj₂ r )) ) ( φ ( FMap F ( λ y → id ) unit , k ))) u→F ⟩ |
| 715 | 405 ( FMap F ( λ r → ( proj₁ r ) ( proj₂ r )) ) ( φ ( FMap F ( λ y → id ) unit , FMap F id u ) ) |
|
717
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
406 ≡⟨ FφF→F ⟩ |
| 713 | 407 FMap F (λ x → proj₂ x ) (φ (unit , u ) ) |
| 408 ≡⟨⟩ | |
| 409 FMap F (Iso.≅→ (mλ-iso isM)) (φ (unit , u )) | |
| 715 | 410 ≡⟨ IsHaskellMonoidalFunctor.idlφ mono ⟩ |
| 713 | 411 u |
| 412 ∎ | |
| 413 where | |
| 414 open Relation.Binary.PropositionalEquality.≡-Reasoning | |
| 415 composition : { a b c : Obj Sets } { u : FObj F ( b → c ) } { v : FObj F (a → b ) } { w : FObj F a } | |
| 416 → (( pure _・_ <*> u ) <*> v ) <*> w ≡ u <*> (v <*> w) | |
| 417 composition {a} {b} {c} {u} {v} {w} = begin | |
| 715 | 418 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ |
| 419 (FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ y f g x → f (g x)) unit , u)) , v)) , w)) | |
| 716 | 420 ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ y f g x → f (g x)) unit , k)) , v)) , w)) ) u→F ⟩ |
| 715 | 421 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ |
| 716 | 422 (FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ y f g x → f (g x)) unit , FMap F id u )) , v)) , w)) |
|
717
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
423 ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ ( k , v)) , w)) ) FφF→F ⟩ |
| 715 | 424 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ |
|
778
06388660995b
fix applicative for Agda version 2.5.4.1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
773
diff
changeset
|
425 (FMap F ( λ x → (λ (r : ((b → c) → _ ) * (b → c) ) → proj₁ r (proj₂ r)) ((map (λ y f g x → f (g x)) id ) x)) (φ ( unit , u)) , v)) , w)) |
| 716 | 426 ≡⟨ ≡-cong ( λ k → ( FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ |
|
778
06388660995b
fix applicative for Agda version 2.5.4.1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
773
diff
changeset
|
427 (FMap F ( λ x → (λ (r : ((b → c) → _ ) * (b → c) ) → proj₁ r (proj₂ r)) ((map (λ y f g x → f (g x)) id ) x)) k , v)) , w)) ) ) φunitr ⟩ |
| 715 | 428 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ |
|
778
06388660995b
fix applicative for Agda version 2.5.4.1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
773
diff
changeset
|
429 ( (FMap F ( λ x → (λ (r : ((b → c) → _ ) * (b → c) ) → proj₁ r (proj₂ r)) ((map (λ y f g x → f (g x)) id ) x)) (FMap F (Iso.≅← (mλ-iso isM)) u) ) , v)) , w)) |
| 716 | 430 ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ |
| 431 (k u , v)) , w)) ) (sym ( IsFunctor.distr (isFunctor F ))) ⟩ | |
| 432 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ | |
| 433 ( FMap F (λ x → ((λ y f g x₁ → f (g x₁)) unit x) ) u , v)) , w)) | |
| 714 | 434 ≡⟨⟩ |
| 715 | 435 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ |
| 716 | 436 ( FMap F (λ x g h → x (g h) ) u , v)) , w)) |
| 437 ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ ( FMap F (λ x g h → x (g h) ) u , k)) , w)) ) u→F ⟩ | |
| 438 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ x g h → x (g h)) u , FMap F id v)) , w)) | |
|
717
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
439 ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (k , w)) ) FφF→F ⟩ |
| 716 | 440 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F ((λ r → proj₁ r (proj₂ r)) o map (λ x g h → x (g h)) id) (φ (u , v)) , w)) |
| 715 | 441 ≡⟨⟩ |
| 716 | 442 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ x h → proj₁ x (proj₂ x h)) (φ (u , v)) , w)) |
| 443 ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ x h → proj₁ x (proj₂ x h)) (φ (u , v)) , k)) ) u→F ⟩ | |
| 444 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ x h → proj₁ x (proj₂ x h)) (φ (u , v)) , FMap F id w)) | |
|
717
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
445 ≡⟨ FφF→F ⟩ |
| 716 | 446 FMap F ((λ r → proj₁ r (proj₂ r)) o map (λ x h → proj₁ x (proj₂ x h)) id) (φ (φ (u , v) , w)) |
| 714 | 447 ≡⟨⟩ |
| 716 | 448 FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (φ (φ (u , v) , w)) |
| 449 ≡⟨ ≡-cong ( λ k → FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (k (φ (φ (u , v) , w)) )) (sym (IsFunctor.identity (isFunctor F ))) ⟩ | |
| 450 FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (FMap F id (φ (φ (u , v) , w)) ) | |
| 451 ≡⟨ ≡-cong ( λ k → FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (FMap F k (φ (φ (u , v) , w)) ) ) (sym (Iso.iso→ (mα-iso isM))) ⟩ | |
| 452 FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (FMap F ( (Iso.≅← (mα-iso isM)) o (Iso.≅→ (mα-iso isM))) (φ (φ (u , v) , w)) ) | |
| 453 ≡⟨ ≡-cong ( λ k → FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (k (φ (φ (u , v) , w)))) ( IsFunctor.distr (isFunctor F )) ⟩ | |
| 454 FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (FMap F (Iso.≅← (mα-iso isM)) ( FMap F (Iso.≅→ (mα-iso isM)) (φ (φ (u , v) , w)) )) | |
| 455 ≡⟨ ≡-cong ( λ k → FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (FMap F (Iso.≅← (mα-iso isM)) k) ) (sym ( IsHaskellMonoidalFunctor.assocφ mono ) ) ⟩ | |
| 456 FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (FMap F (Iso.≅← (mα-iso isM)) (φ (u , φ (v , w)))) | |
| 715 | 457 ≡⟨⟩ |
| 716 | 458 FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (FMap F (λ r → (proj₁ r , proj₁ (proj₂ r)) , proj₂ (proj₂ r)) (φ (u , φ (v , w)))) |
|
721
a8b595fb4905
use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
459 ≡⟨ left (sym ( IsFunctor.distr (isFunctor F ))) ⟩ |
| 716 | 460 FMap F (λ y → (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) ((λ r → (proj₁ r , proj₁ (proj₂ r)) , proj₂ (proj₂ r)) y )) (φ (u , φ (v , w))) |
| 715 | 461 ≡⟨⟩ |
| 716 | 462 FMap F (λ y → proj₁ y (proj₁ (proj₂ y) (proj₂ (proj₂ y)))) (φ (u , φ (v , w))) |
| 715 | 463 ≡⟨⟩ |
| 464 FMap F ( λ x → (proj₁ x) ((λ r → proj₁ r (proj₂ r)) ( proj₂ x))) ( φ ( u , (φ (v , w)))) | |
|
717
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
465 ≡⟨ sym FφF→F ⟩ |
| 715 | 466 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F id u , FMap F (λ r → proj₁ r (proj₂ r)) (φ (v , w)))) |
| 716 | 467 ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (k , FMap F (λ r → proj₁ r (proj₂ r)) (φ (v , w)))) ) (sym u→F ) ⟩ |
| 715 | 468 FMap F (λ r → proj₁ r (proj₂ r)) (φ (u , FMap F (λ r → proj₁ r (proj₂ r)) (φ (v , w)))) |
| 713 | 469 ∎ |
| 470 where | |
| 471 open Relation.Binary.PropositionalEquality.≡-Reasoning | |
| 472 homomorphism : { a b : Obj Sets } { f : Hom Sets a b } { x : a } → pure f <*> pure x ≡ pure (f x) | |
|
717
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
473 homomorphism {a} {b} {f} {x} = begin |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
474 pure f <*> pure x |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
475 ≡⟨⟩ |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
476 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ y → f) unit , FMap F (λ y → x) unit)) |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
477 ≡⟨ FφF→F ⟩ |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
478 FMap F ((λ r → proj₁ r (proj₂ r)) o map (λ y → f) (λ y → x)) (φ (unit , unit)) |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
479 ≡⟨⟩ |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
480 FMap F (λ y → f x) (φ (unit , unit)) |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
481 ≡⟨ ≡-cong ( λ k → FMap F (λ y → f x) k ) φunitl ⟩ |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
482 FMap F (λ y → f x) (FMap F (Iso.≅← (mρ-iso isM)) unit) |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
483 ≡⟨⟩ |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
484 FMap F (λ y → f x) (FMap F (λ y → (y , OneObj)) unit) |
|
721
a8b595fb4905
use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
485 ≡⟨ left ( sym ( IsFunctor.distr (isFunctor F ))) ⟩ |
|
717
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
486 FMap F (λ y → f x) unit |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
487 ≡⟨⟩ |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
488 pure (f x) |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
489 ∎ |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
490 where |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
491 open Relation.Binary.PropositionalEquality.≡-Reasoning |
| 713 | 492 interchange : { a b : Obj Sets } { u : FObj F ( a → b ) } { x : a } → u <*> pure x ≡ pure (λ f → f x) <*> u |
|
717
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
493 interchange {a} {b} {u} {x} = begin |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
494 u <*> pure x |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
495 ≡⟨⟩ |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
496 FMap F (λ r → proj₁ r (proj₂ r)) (φ (u , FMap F (λ y → x) unit)) |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
497 ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (k , FMap F (λ y → x) unit)) ) u→F ⟩ |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
498 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F id u , FMap F (λ y → x) unit)) |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
499 ≡⟨ FφF→F ⟩ |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
500 FMap F ((λ r → proj₁ r (proj₂ r)) o map id (λ y → x)) (φ (u , unit)) |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
501 ≡⟨⟩ |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
502 FMap F (λ r → proj₁ r x) (φ (u , unit)) |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
503 ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r x) k ) φunitl ⟩ |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
504 FMap F (λ r → proj₁ r x) (( FMap F (Iso.≅← (mρ-iso isM))) u ) |
|
721
a8b595fb4905
use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
505 ≡⟨ left ( sym ( IsFunctor.distr (isFunctor F )) ) ⟩ |
|
717
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
506 FMap F (( λ r → proj₁ r x) o ((Iso.≅← (mρ-iso isM) ))) u |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
507 ≡⟨⟩ |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
508 FMap F (( λ r → proj₂ r x) o ((Iso.≅← (mλ-iso isM) ))) u |
|
721
a8b595fb4905
use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
509 ≡⟨ left ( IsFunctor.distr (isFunctor F )) ⟩ |
|
717
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
510 FMap F (λ r → proj₂ r x) (FMap F (Iso.≅← (IsMonoidal.mλ-iso isM)) u) |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
511 ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₂ r x) k ) (sym φunitr ) ⟩ |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
512 FMap F (λ r → proj₂ r x) (φ (unit , u)) |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
513 ≡⟨⟩ |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
514 FMap F ((λ r → proj₁ r (proj₂ r)) o map (λ y f → f x) id) (φ (unit , u)) |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
515 ≡⟨ sym FφF→F ⟩ |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
516 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ y f → f x) unit , FMap F id u)) |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
517 ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ y f → f x) unit , k)) ) (sym u→F) ⟩ |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
518 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ y f → f x) unit , u)) |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
519 ≡⟨⟩ |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
520 pure (λ f → f x) <*> u |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
521 ∎ |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
522 where |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
523 open Relation.Binary.PropositionalEquality.≡-Reasoning |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
524 |
|
765
171f5386e87e
Applicative→HaskellMonoidal begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
732
diff
changeset
|
525 ---- |
|
171f5386e87e
Applicative→HaskellMonoidal begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
732
diff
changeset
|
526 -- |
| 769 | 527 -- Applicative functor implements Haskell Monoidal functor |
| 528 -- Haskell Monoidal functor is directly represents monoidal functor, it is easy to make it from a monoidal functor | |
|
765
171f5386e87e
Applicative→HaskellMonoidal begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
732
diff
changeset
|
529 -- |
|
171f5386e87e
Applicative→HaskellMonoidal begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
732
diff
changeset
|
530 |
|
171f5386e87e
Applicative→HaskellMonoidal begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
732
diff
changeset
|
531 Applicative→HaskellMonoidal : {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) ) |
| 766 | 532 ( App : Applicative F ) |
| 533 → HaskellMonoidalFunctor F | |
| 534 Applicative→HaskellMonoidal {l} F App = record { | |
| 535 unit = unit ; | |
| 536 φ = φ ; | |
| 537 isHaskellMonoidalFunctor = record { | |
|
765
171f5386e87e
Applicative→HaskellMonoidal begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
732
diff
changeset
|
538 natφ = natφ |
|
171f5386e87e
Applicative→HaskellMonoidal begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
732
diff
changeset
|
539 ; assocφ = assocφ |
|
171f5386e87e
Applicative→HaskellMonoidal begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
732
diff
changeset
|
540 ; idrφ = idrφ |
|
171f5386e87e
Applicative→HaskellMonoidal begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
732
diff
changeset
|
541 ; idlφ = idlφ |
| 766 | 542 } |
|
765
171f5386e87e
Applicative→HaskellMonoidal begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
732
diff
changeset
|
543 } where |
| 766 | 544 pure = Applicative.pure App |
| 545 <*> = Applicative.<*> App | |
| 546 app = Applicative.isApplicative App | |
|
765
171f5386e87e
Applicative→HaskellMonoidal begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
732
diff
changeset
|
547 unit : FObj F One |
|
171f5386e87e
Applicative→HaskellMonoidal begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
732
diff
changeset
|
548 unit = pure OneObj |
|
171f5386e87e
Applicative→HaskellMonoidal begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
732
diff
changeset
|
549 φ : {a b : Obj Sets} → Hom Sets ((FObj F a) * (FObj F b )) ( FObj F ( a * b ) ) |
|
171f5386e87e
Applicative→HaskellMonoidal begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
732
diff
changeset
|
550 φ = λ x → <*> (FMap F (λ j k → (j , k)) ( proj₁ x)) ( proj₂ x) |
|
171f5386e87e
Applicative→HaskellMonoidal begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
732
diff
changeset
|
551 isM : IsMonoidal (Sets {l}) One SetsTensorProduct |
|
171f5386e87e
Applicative→HaskellMonoidal begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
732
diff
changeset
|
552 isM = Monoidal.isMonoidal MonoidalSets |
| 766 | 553 MF : MonoidalFunctor {_} {l} {_} {Sets} {Sets} MonoidalSets MonoidalSets |
| 554 MF = Applicative→Monoidal F App app | |
| 555 isMF = MonoidalFunctor.isMonodailFunctor MF | |
|
765
171f5386e87e
Applicative→HaskellMonoidal begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
732
diff
changeset
|
556 natφ : { a b c d : Obj Sets } { x : FObj F a} { y : FObj F b} { f : a → c } { g : b → d } |
|
171f5386e87e
Applicative→HaskellMonoidal begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
732
diff
changeset
|
557 → FMap F (map f g) (φ (x , y)) ≡ φ (FMap F f x , FMap F g y) |
| 766 | 558 natφ {a} {b} {c} {d} {x} {y} {f} {g} = begin |
| 559 FMap F (map f g) (φ (x , y)) | |
| 560 ≡⟨⟩ | |
| 561 FMap F (λ xy → f (proj₁ xy) , g (proj₂ xy)) (<*> (FMap F (λ j k → j , k) x) y) | |
| 562 ≡⟨ ≡-cong ( λ h → h (x , y)) ( IsNTrans.commute ( NTrans.isNTrans ( IsMonoidalFunctor.φab isMF ))) ⟩ | |
| 563 <*> (FMap F (λ j k → j , k) (FMap F f x)) (FMap F g y) | |
| 564 ≡⟨⟩ | |
| 565 φ (FMap F f x , FMap F g y) | |
| 566 ∎ | |
| 567 where | |
| 568 open Relation.Binary.PropositionalEquality.≡-Reasoning | |
|
765
171f5386e87e
Applicative→HaskellMonoidal begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
732
diff
changeset
|
569 assocφ : { x y z : Obj Sets } { a : FObj F x } { b : FObj F y }{ c : FObj F z } |
|
171f5386e87e
Applicative→HaskellMonoidal begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
732
diff
changeset
|
570 → φ (a , φ (b , c)) ≡ FMap F (Iso.≅→ (IsMonoidal.mα-iso isM)) (φ (φ (a , b) , c)) |
| 766 | 571 assocφ {x} {y} {z} {a} {b} {c} = ≡-cong ( λ h → h ((a , b) , c ) ) ( IsMonoidalFunctor.associativity isMF ) |
|
765
171f5386e87e
Applicative→HaskellMonoidal begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
732
diff
changeset
|
572 idrφ : {a : Obj Sets } { x : FObj F a } → FMap F (Iso.≅→ (IsMonoidal.mρ-iso isM)) (φ (x , unit)) ≡ x |
| 766 | 573 idrφ {a} {x} = ≡-cong ( λ h → h (x , OneObj ) ) ( IsMonoidalFunctor.unitarity-idr isMF {a} {One} ) |
|
765
171f5386e87e
Applicative→HaskellMonoidal begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
732
diff
changeset
|
574 idlφ : {a : Obj Sets } { x : FObj F a } → FMap F (Iso.≅→ (IsMonoidal.mλ-iso isM)) (φ (unit , x)) ≡ x |
| 766 | 575 idlφ {a} {x} = ≡-cong ( λ h → h (OneObj , x ) ) ( IsMonoidalFunctor.unitarity-idl isMF {One} {a} ) |
|
765
171f5386e87e
Applicative→HaskellMonoidal begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
732
diff
changeset
|
576 |
| 769 | 577 -- end |