Mercurial > hg > Members > kono > Proof > category
annotate monoidal.agda @ 727:ea84cc6c1797
monoidal functor and applicative done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 26 Nov 2017 16:19:54 +0900 |
| parents | e663c63cdf41 |
| children | 6bc9d68898ef |
| 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 |
|
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
3 module monoidal where |
|
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 |
|
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
11 |
|
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
12 open Functor |
|
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
13 |
| 698 | 14 record Iso {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ) |
| 15 (x y : Obj C ) | |
| 16 : Set ( suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where | |
|
696
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
17 field |
| 698 | 18 ≅→ : Hom C x y |
| 19 ≅← : Hom C y x | |
| 20 iso→ : C [ C [ ≅← o ≅→ ] ≈ id1 C x ] | |
| 21 iso← : C [ C [ ≅→ o ≅← ] ≈ id1 C y ] | |
|
696
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
22 |
| 698 | 23 record IsStrictMonoidal {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ) (I : Obj C) ( BI : Functor ( C × C ) C ) |
|
696
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
24 : Set ( suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where |
|
700
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
25 infixr 9 _□_ |
|
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
26 _□_ : ( x y : Obj C ) → Obj C |
|
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
27 _□_ x y = FObj BI ( x , y ) |
|
696
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
28 field |
|
700
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
29 mα : {a b c : Obj C} → ( a □ b) □ c ≡ a □ ( b □ c ) |
|
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
30 mλ : (a : Obj C) → I □ a ≡ a |
|
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
31 mρ : (a : Obj C) → a □ I ≡ a |
| 698 | 32 |
| 33 record StrictMonoidal {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ) | |
| 34 : Set ( suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where | |
| 35 field | |
| 36 m-i : Obj C | |
| 37 m-bi : Functor ( C × C ) C | |
| 38 isMonoidal : IsStrictMonoidal C m-i m-bi | |
| 39 | |
|
696
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
40 |
| 698 | 41 -- non strict version includes 5 naturalities |
| 42 record IsMonoidal {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ) (I : Obj C) ( BI : Functor ( C × C ) C ) | |
| 43 : Set ( suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where | |
| 44 open Iso | |
|
700
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
45 infixr 9 _□_ _■_ |
|
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
46 _□_ : ( x y : Obj C ) → Obj C |
|
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
47 _□_ x y = FObj BI ( x , y ) |
|
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
48 _■_ : {a b c d : Obj C } ( f : Hom C a c ) ( g : Hom C b d ) → Hom C ( a □ b ) ( c □ d ) |
|
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
49 _■_ f g = FMap BI ( f , g ) |
| 698 | 50 field |
|
700
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
51 mα-iso : {a b c : Obj C} → Iso C ( ( a □ b) □ c) ( a □ ( b □ c ) ) |
|
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
52 mλ-iso : {a : Obj C} → Iso C ( I □ a) a |
|
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
53 mρ-iso : {a : Obj C} → Iso C ( a □ I) a |
| 698 | 54 mα→nat1 : {a a' b c : Obj C} → ( f : Hom C a a' ) → |
|
700
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
55 C [ C [ ( f ■ id1 C ( b □ c )) o ≅→ (mα-iso {a} {b} {c}) ] ≈ |
|
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
56 C [ ≅→ (mα-iso ) o ( (f ■ id1 C b ) ■ id1 C c ) ] ] |
| 698 | 57 mα→nat2 : {a b b' c : Obj C} → ( f : Hom C b b' ) → |
|
700
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
58 C [ C [ ( id1 C a ■ ( f ■ id1 C c ) ) o ≅→ (mα-iso {a} {b} {c} ) ] ≈ |
|
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
59 C [ ≅→ (mα-iso ) o ( (id1 C a ■ f ) ■ id1 C c ) ] ] |
| 698 | 60 mα→nat3 : {a b c c' : Obj C} → ( f : Hom C c c' ) → |
|
700
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
61 C [ C [ ( id1 C a ■ ( id1 C b ■ f ) ) o ≅→ (mα-iso {a} {b} {c} ) ] ≈ |
|
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
62 C [ ≅→ (mα-iso ) o ( id1 C ( a □ b ) ■ f ) ] ] |
| 698 | 63 mλ→nat : {a a' : Obj C} → ( f : Hom C a a' ) → |
| 64 C [ C [ f o ≅→ (mλ-iso {a} ) ] ≈ | |
|
700
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
65 C [ ≅→ (mλ-iso ) o ( id1 C I ■ f ) ] ] |
|
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
66 mρ→nat : {a a' : Obj C} → ( f : Hom C a a' ) → |
|
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
67 C [ C [ f o ≅→ (mρ-iso {a} ) ] ≈ |
|
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
68 C [ ≅→ (mρ-iso ) o ( f ■ id1 C I ) ] ] |
|
705
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
69 -- we should write naturalities for ≅← (maybe derived from above ) |
|
700
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
70 αABC□1D : {a b c d e : Obj C } → Hom C (((a □ b) □ c ) □ d) ((a □ (b □ c)) □ d) |
|
701
7a729bb62ce3
Monoidal Functor on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
700
diff
changeset
|
71 αABC□1D {a} {b} {c} {d} {e} = ( ≅→ mα-iso ■ id1 C d ) |
|
700
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
72 αAB□CD : {a b c d e : Obj C } → Hom C ((a □ (b □ c)) □ d) (a □ ((b □ c ) □ d)) |
|
701
7a729bb62ce3
Monoidal Functor on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
700
diff
changeset
|
73 αAB□CD {a} {b} {c} {d} {e} = ≅→ mα-iso |
|
700
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
74 1A□BCD : {a b c d e : Obj C } → Hom C (a □ ((b □ c ) □ d)) (a □ (b □ ( c □ d) )) |
|
701
7a729bb62ce3
Monoidal Functor on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
700
diff
changeset
|
75 1A□BCD {a} {b} {c} {d} {e} = ( id1 C a ■ ≅→ mα-iso ) |
|
700
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
76 αABC□D : {a b c d e : Obj C } → Hom C (a □ (b □ ( c □ d) )) ((a □ b ) □ (c □ d)) |
|
701
7a729bb62ce3
Monoidal Functor on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
700
diff
changeset
|
77 αABC□D {a} {b} {c} {d} {e} = ≅← mα-iso |
|
700
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
78 αA□BCD : {a b c d e : Obj C } → Hom C (((a □ b) □ c ) □ d) ((a □ b ) □ (c □ d)) |
|
701
7a729bb62ce3
Monoidal Functor on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
700
diff
changeset
|
79 αA□BCD {a} {b} {c} {d} {e} = ≅→ mα-iso |
|
700
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
80 αAIB : {a b : Obj C } → Hom C (( a □ I ) □ b ) (a □ ( I □ b )) |
|
701
7a729bb62ce3
Monoidal Functor on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
700
diff
changeset
|
81 αAIB {a} {b} = ≅→ mα-iso |
|
700
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
82 1A□λB : {a b : Obj C } → Hom C (a □ ( I □ b )) ( a □ b ) |
|
701
7a729bb62ce3
Monoidal Functor on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
700
diff
changeset
|
83 1A□λB {a} {b} = id1 C a ■ ≅→ mλ-iso |
|
700
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
84 ρA□IB : {a b : Obj C } → Hom C (( a □ I ) □ b ) ( a □ b ) |
|
701
7a729bb62ce3
Monoidal Functor on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
700
diff
changeset
|
85 ρA□IB {a} {b} = ≅→ mρ-iso ■ id1 C b |
|
700
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
86 |
|
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
87 field |
|
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
88 comm-penta : {a b c d e : Obj C} |
|
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
89 → C [ C [ αABC□D {a} {b} {c} {d} {e} o C [ 1A□BCD {a} {b} {c} {d} {e} o C [ αAB□CD {a} {b} {c} {d} {e} o αABC□1D {a} {b} {c} {d} {e} ] ] ] |
|
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
90 ≈ αA□BCD {a} {b} {c} {d} {e} ] |
|
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
91 comm-unit : {a b : Obj C} |
|
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
92 → C [ C [ 1A□λB {a} {b} o αAIB ] ≈ ρA□IB {a} {b} ] |
|
696
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
93 |
|
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
94 record Monoidal {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ) |
|
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
95 : Set ( suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where |
|
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
96 field |
|
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
97 m-i : Obj C |
|
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
98 m-bi : Functor ( C × C ) C |
|
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
99 isMonoidal : IsMonoidal C m-i m-bi |
|
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
100 |
|
705
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
101 --------- |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
102 -- |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
103 -- Lax Monoidal Functor |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
104 -- |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
105 -- N → M |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
106 -- |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
107 --------- |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
108 |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
109 --------- |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
110 -- |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
111 -- Two implementations of Functor ( C × C ) → D from F : Functor C → D (given) |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
112 -- dervied from F and two Monoidal Categories |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
113 -- |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
114 -- F x ● F y |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
115 -- F ( x ⊗ y ) |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
116 -- |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
117 -- and a given natural transformation for them |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
118 -- |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
119 -- φ : F x ● F y → F ( x ⊗ y ) |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
120 -- |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
121 -- TMap φ : ( x y : Obj C ) → Hom D ( F x ● F y ) ( F ( x ⊗ y )) |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
122 -- |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
123 -- a given unit arrow |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
124 -- |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
125 -- ψ : IN → IM |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
126 |
| 703 | 127 Functor● : {c₁ c₂ ℓ : Level} (C D : Category c₁ c₂ ℓ) ( N : Monoidal D ) |
| 128 ( MF : Functor C D ) → Functor ( C × C ) D | |
| 129 Functor● C D N MF = record { | |
| 130 FObj = λ x → (FObj MF (proj₁ x) ) ● (FObj MF (proj₂ x) ) | |
|
705
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
131 ; FMap = λ {x : Obj ( C × C ) } {y} f → ( FMap MF (proj₁ f ) ■ FMap MF (proj₂ f) ) |
| 703 | 132 ; isFunctor = record { |
| 133 ≈-cong = ≈-cong | |
| 134 ; identity = identity | |
| 135 ; distr = distr | |
| 136 } | |
| 137 } where | |
| 138 _●_ : (x y : Obj D ) → Obj D | |
| 139 _●_ x y = (IsMonoidal._□_ (Monoidal.isMonoidal N) ) x y | |
| 704 | 140 _■_ : {a b c d : Obj D } ( f : Hom D a c ) ( g : Hom D b d ) → Hom D ( a ● b ) ( c ● d ) |
| 141 _■_ f g = FMap (Monoidal.m-bi N) ( f , g ) | |
| 142 F : { a b : Obj C } → ( f : Hom C a b ) → Hom D (FObj MF a) (FObj MF b ) | |
| 143 F f = FMap MF f | |
| 703 | 144 ≈-cong : {a b : Obj (C × C)} {f g : Hom (C × C) a b} → (C × C) [ f ≈ g ] → |
| 704 | 145 D [ (F (proj₁ f) ■ F (proj₂ f)) ≈ (F (proj₁ g) ■ F (proj₂ g)) ] |
| 703 | 146 ≈-cong {a} {b} {f} {g} f≈g = let open ≈-Reasoning D in begin |
| 704 | 147 F (proj₁ f) ■ F (proj₂ f) |
| 703 | 148 ≈⟨ fcong (Monoidal.m-bi N) ( fcong MF ( proj₁ f≈g ) , fcong MF ( proj₂ f≈g )) ⟩ |
| 704 | 149 F (proj₁ g) ■ F (proj₂ g) |
| 703 | 150 ∎ |
| 704 | 151 identity : {a : Obj (C × C)} → D [ (F (proj₁ (id1 (C × C) a)) ■ F (proj₂ (id1 (C × C) a))) |
| 703 | 152 ≈ id1 D (FObj MF (proj₁ a) ● FObj MF (proj₂ a)) ] |
| 153 identity {a} = let open ≈-Reasoning D in begin | |
| 704 | 154 F (proj₁ (id1 (C × C) a)) ■ F (proj₂ (id1 (C × C) a)) |
| 703 | 155 ≈⟨ fcong (Monoidal.m-bi N) ( IsFunctor.identity (isFunctor MF ) , IsFunctor.identity (isFunctor MF )) ⟩ |
| 704 | 156 id1 D (FObj MF (proj₁ a)) ■ id1 D (FObj MF (proj₂ a)) |
| 703 | 157 ≈⟨ IsFunctor.identity (isFunctor (Monoidal.m-bi N)) ⟩ |
| 158 id1 D (FObj MF (proj₁ a) ● FObj MF (proj₂ a)) | |
| 159 ∎ | |
| 160 distr : {a b c : Obj (C × C)} {f : Hom (C × C) a b} {g : Hom (C × C) b c} → | |
| 704 | 161 D [ (F (proj₁ ((C × C) [ g o f ])) ■ F (proj₂ ((C × C) [ g o f ]))) |
| 162 ≈ D [ (F (proj₁ g) ■ F (proj₂ g)) o (F (proj₁ f) ■ F (proj₂ f)) ] ] | |
| 703 | 163 distr {a} {b} {c} {f} {g} = let open ≈-Reasoning D in begin |
| 704 | 164 (F (proj₁ ((C × C) [ g o f ])) ■ F (proj₂ ((C × C) [ g o f ]))) |
| 703 | 165 ≈⟨ fcong (Monoidal.m-bi N) ( IsFunctor.distr ( isFunctor MF) , IsFunctor.distr ( isFunctor MF )) ⟩ |
| 704 | 166 ( F (proj₁ g) o F (proj₁ f) ) ■ ( F (proj₂ g) o F (proj₂ f) ) |
| 703 | 167 ≈⟨ IsFunctor.distr ( isFunctor (Monoidal.m-bi N)) ⟩ |
| 704 | 168 (F (proj₁ g) ■ F (proj₂ g)) o (F (proj₁ f) ■ F (proj₂ f)) |
| 703 | 169 ∎ |
|
696
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
170 |
| 703 | 171 Functor⊗ : {c₁ c₂ ℓ : Level} (C D : Category c₁ c₂ ℓ) ( M : Monoidal C ) |
| 172 ( MF : Functor C D ) → Functor ( C × C ) D | |
| 173 Functor⊗ C D M MF = record { | |
| 174 FObj = λ x → FObj MF ( proj₁ x ⊗ proj₂ x ) | |
|
705
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
175 ; FMap = λ {a} {b} f → F ( proj₁ f □ proj₂ f ) |
| 703 | 176 ; isFunctor = record { |
| 177 ≈-cong = ≈-cong | |
| 178 ; identity = identity | |
| 179 ; distr = distr | |
| 180 } | |
| 181 } where | |
| 182 _⊗_ : (x y : Obj C ) → Obj C | |
| 183 _⊗_ x y = (IsMonoidal._□_ (Monoidal.isMonoidal M) ) x y | |
| 704 | 184 _□_ : {a b c d : Obj C } ( f : Hom C a c ) ( g : Hom C b d ) → Hom C ( a ⊗ b ) ( c ⊗ d ) |
| 185 _□_ f g = FMap (Monoidal.m-bi M) ( f , g ) | |
| 186 F : { a b : Obj C } → ( f : Hom C a b ) → Hom D (FObj MF a) (FObj MF b ) | |
| 187 F f = FMap MF f | |
| 703 | 188 ≈-cong : {a b : Obj (C × C)} {f g : Hom (C × C) a b} → (C × C) [ f ≈ g ] → |
| 704 | 189 D [ F ( (proj₁ f □ proj₂ f)) ≈ F ( (proj₁ g □ proj₂ g)) ] |
| 703 | 190 ≈-cong {a} {b} {f} {g} f≈g = IsFunctor.≈-cong (isFunctor MF ) ( IsFunctor.≈-cong (isFunctor (Monoidal.m-bi M) ) f≈g ) |
| 704 | 191 identity : {a : Obj (C × C)} → D [ F ( (proj₁ (id1 (C × C) a) □ proj₂ (id1 (C × C) a))) |
| 703 | 192 ≈ id1 D (FObj MF (proj₁ a ⊗ proj₂ a)) ] |
| 193 identity {a} = let open ≈-Reasoning D in begin | |
| 704 | 194 F ( (proj₁ (id1 (C × C) a) □ proj₂ (id1 (C × C) a))) |
| 703 | 195 ≈⟨⟩ |
| 704 | 196 F (FMap (Monoidal.m-bi M) (id1 (C × C) a ) ) |
| 703 | 197 ≈⟨ fcong MF ( IsFunctor.identity (isFunctor (Monoidal.m-bi M) )) ⟩ |
| 704 | 198 F (id1 C (proj₁ a ⊗ proj₂ a)) |
| 703 | 199 ≈⟨ IsFunctor.identity (isFunctor MF) ⟩ |
| 200 id1 D (FObj MF (proj₁ a ⊗ proj₂ a)) | |
| 201 ∎ | |
| 202 distr : {a b c : Obj (C × C)} {f : Hom (C × C) a b} {g : Hom (C × C) b c} → D [ | |
| 704 | 203 F ( (proj₁ ((C × C) [ g o f ]) □ proj₂ ((C × C) [ g o f ]))) |
| 204 ≈ D [ F ( (proj₁ g □ proj₂ g)) o F ( (proj₁ f □ proj₂ f)) ] ] | |
| 703 | 205 distr {a} {b} {c} {f} {g} = let open ≈-Reasoning D in begin |
| 704 | 206 F ( (proj₁ ((C × C) [ g o f ]) □ proj₂ ((C × C) [ g o f ]))) |
| 703 | 207 ≈⟨⟩ |
| 704 | 208 F (FMap (Monoidal.m-bi M) ( (C × C) [ g o f ] )) |
| 703 | 209 ≈⟨ fcong MF ( IsFunctor.distr (isFunctor (Monoidal.m-bi M))) ⟩ |
| 704 | 210 F (C [ FMap (Monoidal.m-bi M) g o FMap (Monoidal.m-bi M) f ]) |
| 703 | 211 ≈⟨ IsFunctor.distr ( isFunctor MF ) ⟩ |
| 704 | 212 F ( proj₁ g □ proj₂ g) o F ( proj₁ f □ proj₂ f) |
| 703 | 213 ∎ |
| 214 | |
|
696
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
215 |
|
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
216 record IsMonoidalFunctor {c₁ c₂ ℓ : Level} {C D : Category c₁ c₂ ℓ} ( M : Monoidal C ) ( N : Monoidal D ) |
| 698 | 217 ( MF : Functor C D ) |
|
702
d16327b48b83
Monoidal Functor ( two functor remains )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
701
diff
changeset
|
218 ( ψ : Hom D (Monoidal.m-i N) (FObj MF (Monoidal.m-i M) ) ) |
|
696
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
219 : Set ( suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where |
| 698 | 220 _⊗_ : (x y : Obj C ) → Obj C |
|
700
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
221 _⊗_ x y = (IsMonoidal._□_ (Monoidal.isMonoidal M) ) x y |
|
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
222 _□_ : {a b c d : Obj C } ( f : Hom C a c ) ( g : Hom C b d ) → Hom C ( a ⊗ b ) ( c ⊗ d ) |
|
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
223 _□_ f g = FMap (Monoidal.m-bi M) ( f , g ) |
| 698 | 224 _●_ : (x y : Obj D ) → Obj D |
|
700
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
225 _●_ x y = (IsMonoidal._□_ (Monoidal.isMonoidal N) ) x y |
|
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
226 _■_ : {a b c d : Obj D } ( f : Hom D a c ) ( g : Hom D b d ) → Hom D ( a ● b ) ( c ● d ) |
|
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
227 _■_ f g = FMap (Monoidal.m-bi N) ( f , g ) |
|
702
d16327b48b83
Monoidal Functor ( two functor remains )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
701
diff
changeset
|
228 F● : Functor ( C × C ) D |
| 703 | 229 F● = Functor● C D N MF |
|
702
d16327b48b83
Monoidal Functor ( two functor remains )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
701
diff
changeset
|
230 F⊗ : Functor ( C × C ) D |
| 703 | 231 F⊗ = Functor⊗ C D M MF |
|
702
d16327b48b83
Monoidal Functor ( two functor remains )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
701
diff
changeset
|
232 field |
|
d16327b48b83
Monoidal Functor ( two functor remains )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
701
diff
changeset
|
233 φab : NTrans ( C × C ) D F● F⊗ |
| 698 | 234 open Iso |
| 235 open Monoidal | |
|
701
7a729bb62ce3
Monoidal Functor on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
700
diff
changeset
|
236 open IsMonoidal hiding ( _■_ ; _□_ ) |
| 699 | 237 αC : {a b c : Obj C} → Hom C (( a ⊗ b ) ⊗ c ) ( a ⊗ ( b ⊗ c ) ) |
| 238 αC {a} {b} {c} = ≅→ (mα-iso (isMonoidal M) {a} {b} {c}) | |
| 239 αD : {a b c : Obj D} → Hom D (( a ● b ) ● c ) ( a ● ( b ● c ) ) | |
| 240 αD {a} {b} {c} = ≅→ (mα-iso (isMonoidal N) {a} {b} {c}) | |
|
701
7a729bb62ce3
Monoidal Functor on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
700
diff
changeset
|
241 F : Obj C → Obj D |
|
7a729bb62ce3
Monoidal Functor on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
700
diff
changeset
|
242 F x = FObj MF x |
|
702
d16327b48b83
Monoidal Functor ( two functor remains )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
701
diff
changeset
|
243 φ : ( x y : Obj C ) → Hom D ( FObj F● (x , y) ) ( FObj F⊗ ( x , y )) |
|
d16327b48b83
Monoidal Functor ( two functor remains )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
701
diff
changeset
|
244 φ x y = NTrans.TMap φab ( x , y ) |
|
701
7a729bb62ce3
Monoidal Functor on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
700
diff
changeset
|
245 1●φBC : {a b c : Obj C} → Hom D ( F a ● ( F b ● F c ) ) ( F a ● ( F ( b ⊗ c ) )) |
|
702
d16327b48b83
Monoidal Functor ( two functor remains )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
701
diff
changeset
|
246 1●φBC {a} {b} {c} = id1 D (F a) ■ φ b c |
|
701
7a729bb62ce3
Monoidal Functor on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
700
diff
changeset
|
247 φAB⊗C : {a b c : Obj C} → Hom D ( F a ● ( F ( b ⊗ c ) )) (F ( a ⊗ ( b ⊗ c ))) |
|
702
d16327b48b83
Monoidal Functor ( two functor remains )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
701
diff
changeset
|
248 φAB⊗C {a} {b} {c} = φ a (b ⊗ c ) |
|
701
7a729bb62ce3
Monoidal Functor on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
700
diff
changeset
|
249 φAB●1 : {a b c : Obj C} → Hom D ( ( F a ● F b ) ● F c ) ( F ( a ⊗ b ) ● F c ) |
|
702
d16327b48b83
Monoidal Functor ( two functor remains )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
701
diff
changeset
|
250 φAB●1 {a} {b} {c} = φ a b ■ id1 D (F c) |
|
701
7a729bb62ce3
Monoidal Functor on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
700
diff
changeset
|
251 φA⊗BC : {a b c : Obj C} → Hom D ( F ( a ⊗ b ) ● F c ) (F ( (a ⊗ b ) ⊗ c )) |
|
702
d16327b48b83
Monoidal Functor ( two functor remains )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
701
diff
changeset
|
252 φA⊗BC {a} {b} {c} = φ ( a ⊗ b ) c |
|
701
7a729bb62ce3
Monoidal Functor on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
700
diff
changeset
|
253 FαC : {a b c : Obj C} → Hom D (F ( (a ⊗ b ) ⊗ c )) (F ( a ⊗ ( b ⊗ c ))) |
|
7a729bb62ce3
Monoidal Functor on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
700
diff
changeset
|
254 FαC {a} {b} {c} = FMap MF ( ≅→ (mα-iso (isMonoidal M) {a} {b} {c}) ) |
|
702
d16327b48b83
Monoidal Functor ( two functor remains )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
701
diff
changeset
|
255 1●ψ : { a b : Obj C } → Hom D (F a ● Monoidal.m-i N ) ( F a ● F ( Monoidal.m-i M ) ) |
|
d16327b48b83
Monoidal Functor ( two functor remains )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
701
diff
changeset
|
256 1●ψ{a} {b} = id1 D (F a) ■ ψ |
|
701
7a729bb62ce3
Monoidal Functor on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
700
diff
changeset
|
257 φAIC : { a b : Obj C } → Hom D ( F a ● F ( Monoidal.m-i M ) ) (F ( a ⊗ Monoidal.m-i M )) |
|
702
d16327b48b83
Monoidal Functor ( two functor remains )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
701
diff
changeset
|
258 φAIC {a} {b} = φ a ( Monoidal.m-i M ) |
|
701
7a729bb62ce3
Monoidal Functor on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
700
diff
changeset
|
259 FρC : { a b : Obj C } → Hom D (F ( a ⊗ Monoidal.m-i M ))( F a ) |
|
7a729bb62ce3
Monoidal Functor on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
700
diff
changeset
|
260 FρC {a} {b} = FMap MF ( ≅→ (mρ-iso (isMonoidal M) {a} ) ) |
|
7a729bb62ce3
Monoidal Functor on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
700
diff
changeset
|
261 ρD : { a b : Obj C } → Hom D (F a ● Monoidal.m-i N ) ( F a ) |
|
7a729bb62ce3
Monoidal Functor on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
700
diff
changeset
|
262 ρD {a} {b} = ≅→ (mρ-iso (isMonoidal N) {F a} ) |
|
702
d16327b48b83
Monoidal Functor ( two functor remains )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
701
diff
changeset
|
263 ψ●1 : { a b : Obj C } → Hom D (Monoidal.m-i N ● F b ) ( F ( Monoidal.m-i M ) ● F b ) |
|
d16327b48b83
Monoidal Functor ( two functor remains )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
701
diff
changeset
|
264 ψ●1 {a} {b} = ψ ■ id1 D (F b) |
|
701
7a729bb62ce3
Monoidal Functor on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
700
diff
changeset
|
265 φICB : { a b : Obj C } → Hom D ( F ( Monoidal.m-i M ) ● F b ) ( F ( ( Monoidal.m-i M ) ⊗ b ) ) |
|
702
d16327b48b83
Monoidal Functor ( two functor remains )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
701
diff
changeset
|
266 φICB {a} {b} = φ ( Monoidal.m-i M ) b |
|
701
7a729bb62ce3
Monoidal Functor on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
700
diff
changeset
|
267 FλD : { a b : Obj C } → Hom D ( F ( ( Monoidal.m-i M ) ⊗ b ) ) (F b ) |
|
7a729bb62ce3
Monoidal Functor on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
700
diff
changeset
|
268 FλD {a} {b} = FMap MF ( ≅→ (mλ-iso (isMonoidal M) {b} ) ) |
|
7a729bb62ce3
Monoidal Functor on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
700
diff
changeset
|
269 λD : { a b : Obj C } → Hom D (Monoidal.m-i N ● F b ) (F b ) |
|
7a729bb62ce3
Monoidal Functor on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
700
diff
changeset
|
270 λD {a} {b} = ≅→ (mλ-iso (isMonoidal N) {F b} ) |
|
696
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
271 field |
|
705
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
272 associativity : {a b c : Obj C } → D [ D [ φAB⊗C {a} {b} {c} o D [ 1●φBC o αD ] ] ≈ D [ FαC o D [ φA⊗BC o φAB●1 ] ] ] |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
273 unitarity-idr : {a b : Obj C } → D [ D [ FρC {a} {b} o D [ φAIC {a} {b} o 1●ψ{a} {b} ] ] ≈ ρD {a} {b} ] |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
274 unitarity-idl : {a b : Obj C } → D [ D [ FλD {a} {b} o D [ φICB {a} {b} o ψ●1 {a} {b} ] ] ≈ λD {a} {b} ] |
|
696
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
275 |
|
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
276 record MonoidalFunctor {c₁ c₂ ℓ : Level} {C D : Category c₁ c₂ ℓ} ( M : Monoidal C ) ( N : Monoidal D ) |
|
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
277 : Set ( suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where |
|
705
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
278 field |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
279 MF : Functor C D |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
280 ψ : Hom D (Monoidal.m-i N) (FObj MF (Monoidal.m-i M) ) |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
281 isMonodailFunctor : IsMonoidalFunctor M N MF ψ |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
282 |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
283 record MonoidalFunctorWithoutCommutativities {c₁ c₂ ℓ : Level} {C D : Category c₁ c₂ ℓ} ( M : Monoidal C ) ( N : Monoidal D ) |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
284 : Set ( suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where |
|
696
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
285 _⊗_ : (x y : Obj C ) → Obj C |
|
700
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
286 _⊗_ x y = (IsMonoidal._□_ (Monoidal.isMonoidal M) ) x y |
|
696
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
287 _●_ : (x y : Obj D ) → Obj D |
|
700
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
288 _●_ x y = (IsMonoidal._□_ (Monoidal.isMonoidal N) ) x y |
|
696
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
289 field |
|
705
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
290 MF : Functor C D |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
291 unit : Hom D (Monoidal.m-i N) (FObj MF (Monoidal.m-i M) ) |
| 708 | 292 φ : {a b : Obj C} → Hom D ((FObj MF a) ● (FObj MF b )) ( FObj MF ( a ⊗ b ) ) |
|
705
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
293 |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
294 open import Category.Sets |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
295 |
| 706 | 296 import Relation.Binary.PropositionalEquality |
| 297 -- Extensionality a b = {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → f ≡ g → ( λ x → f x ≡ λ x → g x ) | |
| 298 postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂ | |
| 299 | |
|
705
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
300 data One {c : Level} : Set c where |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
301 OneObj : One -- () in Haskell ( or any one object set ) |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
302 |
| 708 | 303 SetsTensorProduct : {c : Level} → Functor ( Sets {c} × Sets {c} ) (Sets {c}) |
| 304 SetsTensorProduct = record { | |
| 305 FObj = λ x → proj₁ x * proj₂ x | |
| 306 ; FMap = λ {x : Obj ( Sets × Sets ) } {y} f → map (proj₁ f) (proj₂ f) | |
| 307 ; isFunctor = record { | |
| 308 ≈-cong = ≈-cong | |
| 309 ; identity = refl | |
| 310 ; distr = refl | |
| 706 | 311 } |
| 708 | 312 } where |
| 313 ≈-cong : {a b : Obj (Sets × Sets)} {f g : Hom (Sets × Sets) a b} → | |
| 314 (Sets × Sets) [ f ≈ g ] → Sets [ map (proj₁ f) (proj₂ f) ≈ map (proj₁ g) (proj₂ g) ] | |
| 315 ≈-cong (refl , refl) = refl | |
| 316 | |
| 317 | |
| 318 | |
| 319 MonoidalSets : {c : Level} → Monoidal (Sets {c}) | |
|
727
ea84cc6c1797
monoidal functor and applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
726
diff
changeset
|
320 MonoidalSets {c} = record { |
|
ea84cc6c1797
monoidal functor and applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
726
diff
changeset
|
321 m-i = One {c} ; |
| 708 | 322 m-bi = SetsTensorProduct ; |
| 323 isMonoidal = record { | |
| 324 mα-iso = record { ≅→ = mα→ ; ≅← = mα← ; iso→ = refl ; iso← = refl } ; | |
| 325 mλ-iso = record { ≅→ = mλ→ ; ≅← = mλ← ; iso→ = extensionality Sets ( λ x → mλiso x ) ; iso← = refl } ; | |
| 326 mρ-iso = record { ≅→ = mρ→ ; ≅← = mρ← ; iso→ = extensionality Sets ( λ x → mρiso x ) ; iso← = refl } ; | |
| 327 mα→nat1 = λ f → refl ; | |
| 328 mα→nat2 = λ f → refl ; | |
| 329 mα→nat3 = λ f → refl ; | |
| 330 mλ→nat = λ f → refl ; | |
| 331 mρ→nat = λ f → refl ; | |
| 332 comm-penta = refl ; | |
| 333 comm-unit = refl | |
| 334 } | |
| 335 } where | |
| 336 _⊗_ : ( a b : Obj Sets ) → Obj Sets | |
| 337 _⊗_ a b = FObj SetsTensorProduct (a , b ) | |
| 338 mα→ : {a b c : Obj Sets} → Hom Sets ( ( a ⊗ b ) ⊗ c ) ( a ⊗ ( b ⊗ c ) ) | |
| 339 mα→ ((a , b) , c ) = (a , ( b , c ) ) | |
| 340 mα← : {a b c : Obj Sets} → Hom Sets ( a ⊗ ( b ⊗ c ) ) ( ( a ⊗ b ) ⊗ c ) | |
| 341 mα← (a , ( b , c ) ) = ((a , b) , c ) | |
| 342 mλ→ : {a : Obj Sets} → Hom Sets ( One ⊗ a ) a | |
| 343 mλ→ (_ , a) = a | |
| 344 mλ← : {a : Obj Sets} → Hom Sets a ( One ⊗ a ) | |
| 345 mλ← a = ( OneObj , a ) | |
| 346 mλiso : {a : Obj Sets} (x : One ⊗ a) → (Sets [ mλ← o mλ→ ]) x ≡ id1 Sets (One ⊗ a) x | |
| 347 mλiso (OneObj , _ ) = refl | |
| 348 mρ→ : {a : Obj Sets} → Hom Sets ( a ⊗ One ) a | |
| 349 mρ→ (a , _) = a | |
| 350 mρ← : {a : Obj Sets} → Hom Sets a ( a ⊗ One ) | |
| 351 mρ← a = ( a , OneObj ) | |
| 352 mρiso : {a : Obj Sets} (x : a ⊗ One ) → (Sets [ mρ← o mρ→ ]) x ≡ id1 Sets (a ⊗ One) x | |
| 353 mρiso (_ , OneObj ) = refl | |
| 354 | |
| 710 | 355 ≡-cong = Relation.Binary.PropositionalEquality.cong |
| 706 | 356 |
| 713 | 357 |
| 358 record IsHaskellMonoidalFunctor {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) ) | |
| 359 ( unit : FObj F One ) | |
| 360 ( φ : {a b : Obj Sets} → Hom Sets ((FObj F a) * (FObj F b )) ( FObj F ( a * b ) ) ) | |
| 361 : Set (suc (suc c₁)) where | |
| 362 isM : IsMonoidal (Sets {c₁}) One SetsTensorProduct | |
| 363 isM = Monoidal.isMonoidal MonoidalSets | |
| 364 open IsMonoidal | |
| 365 field | |
| 715 | 366 natφ : { a b c d : Obj Sets } { x : FObj F a} { y : FObj F b} { f : a → c } { g : b → d } |
| 713 | 367 → FMap F (map f g) (φ (x , y)) ≡ φ (FMap F f x , FMap F g y) |
| 715 | 368 assocφ : { x y z : Obj Sets } { a : FObj F x } { b : FObj F y }{ c : FObj F z } |
| 713 | 369 → φ (a , φ (b , c)) ≡ FMap F (Iso.≅→ (mα-iso isM)) (φ (φ (a , b) , c)) |
| 715 | 370 idrφ : {a : Obj Sets } { x : FObj F a } → FMap F (Iso.≅→ (mρ-iso isM)) (φ (x , unit)) ≡ x |
| 371 idlφ : {a : Obj Sets } { x : FObj F a } → FMap F (Iso.≅→ (mλ-iso isM)) (φ (unit , x)) ≡ x | |
| 713 | 372 |
| 714 | 373 -- http://www.staff.city.ac.uk/~ross/papers/Applicative.pdf |
| 374 -- naturality of φ fmap(f × g)(φ u v) = φ ( fmap f u) ( fmap g v ) | |
| 375 -- left identity fmap snd (φ unit v) = v | |
| 376 -- right identity fmap fst (φ u unit) = u | |
| 377 -- associativity fmap assoc (φ u (φ v w)) = φ (φ u v) w | |
| 378 | |
| 379 | |
|
705
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
380 record HaskellMonoidalFunctor {c₁ : Level} ( f : Functor (Sets {c₁}) (Sets {c₁}) ) |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
381 : Set (suc (suc c₁)) where |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
382 field |
| 706 | 383 unit : FObj f One |
|
705
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
384 φ : {a b : Obj Sets} → Hom Sets ((FObj f a) * (FObj f b )) ( FObj f ( a * b ) ) |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
385 ** : {a b : Obj Sets} → FObj f a → FObj f b → FObj f ( a * b ) |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
386 ** x y = φ ( x , y ) |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
387 |
| 713 | 388 lemma0 : {c : Level} ( F : Functor (Sets {c}) (Sets {c}) ) → (mf : HaskellMonoidalFunctor F ) |
| 389 → IsHaskellMonoidalFunctor F ( HaskellMonoidalFunctor.unit mf ) ( HaskellMonoidalFunctor.φ mf ) | |
| 390 → MonoidalFunctor {_} {c} {_} {Sets} {Sets} MonoidalSets MonoidalSets | |
| 391 lemma0 F mf ismf = record { | |
| 709 | 392 MF = F |
| 393 ; ψ = λ _ → HaskellMonoidalFunctor.unit mf | |
| 394 ; isMonodailFunctor = record { | |
| 711 | 395 φab = record { TMap = λ x → φ ; isNTrans = record { commute = comm0 } } |
| 396 ; associativity = λ {a b c} → comm1 {a} {b} {c} | |
| 710 | 397 ; unitarity-idr = λ {a b} → comm2 {a} {b} |
| 398 ; unitarity-idl = λ {a b} → comm3 {a} {b} | |
| 709 | 399 } |
| 400 } where | |
| 401 open Monoidal | |
| 402 open IsMonoidal hiding ( _■_ ; _□_ ) | |
| 403 M = MonoidalSets | |
| 404 isM = Monoidal.isMonoidal MonoidalSets | |
| 405 unit = HaskellMonoidalFunctor.unit mf | |
| 406 _⊗_ : (x y : Obj Sets ) → Obj Sets | |
| 407 _⊗_ x y = (IsMonoidal._□_ (Monoidal.isMonoidal M) ) x y | |
| 408 _□_ : {a b c d : Obj Sets } ( f : Hom Sets a c ) ( g : Hom Sets b d ) → Hom Sets ( a ⊗ b ) ( c ⊗ d ) | |
| 409 _□_ f g = FMap (m-bi M) ( f , g ) | |
| 711 | 410 φ : {x : Obj (Sets × Sets) } → Hom Sets (FObj (Functor● Sets Sets MonoidalSets F) x) (FObj (Functor⊗ Sets Sets MonoidalSets F) x) |
| 411 φ z = HaskellMonoidalFunctor.φ mf z | |
| 710 | 412 comm00 : {a b : Obj (Sets × Sets)} { f : Hom (Sets × Sets) a b} (x : ( FObj F (proj₁ a) * FObj F (proj₂ a)) ) → |
| 711 | 413 (Sets [ FMap (Functor⊗ Sets Sets MonoidalSets F) f o φ ]) x ≡ (Sets [ φ o FMap (Functor● Sets Sets MonoidalSets F) f ]) x |
| 710 | 414 comm00 {a} {b} {(f , g)} (x , y) = begin |
| 711 | 415 (FMap (Functor⊗ Sets Sets MonoidalSets F) (f , g) ) (φ (x , y)) |
| 710 | 416 ≡⟨⟩ |
| 711 | 417 (FMap F ( f □ g ) ) (φ (x , y)) |
| 710 | 418 ≡⟨⟩ |
| 711 | 419 FMap F ( map f g ) (φ (x , y)) |
| 715 | 420 ≡⟨ IsHaskellMonoidalFunctor.natφ ismf ⟩ |
| 711 | 421 φ ( FMap F f x , FMap F g y ) |
| 710 | 422 ≡⟨⟩ |
| 711 | 423 φ ( ( FMap F f □ FMap F g ) (x , y) ) |
| 710 | 424 ≡⟨⟩ |
| 711 | 425 φ ((FMap (Functor● Sets Sets MonoidalSets F) (f , g) ) (x , y) ) |
| 710 | 426 ∎ |
| 427 where | |
| 713 | 428 open Relation.Binary.PropositionalEquality.≡-Reasoning |
| 711 | 429 comm0 : {a b : Obj (Sets × Sets)} { f : Hom (Sets × Sets) a b} → Sets [ Sets [ FMap (Functor⊗ Sets Sets MonoidalSets F) f o φ ] |
| 430 ≈ Sets [ φ o FMap (Functor● Sets Sets MonoidalSets F) f ] ] | |
| 710 | 431 comm0 {a} {b} {f} = extensionality Sets ( λ (x : ( FObj F (proj₁ a) * FObj F (proj₂ a)) ) → comm00 x ) |
| 711 | 432 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 ≡ |
| 433 (Sets [ FMap F (Iso.≅→ (mα-iso isM)) o Sets [ φ o φ □ id1 Sets (FObj F c) ] ]) x | |
| 710 | 434 comm10 {x} {y} {f} ((a , b) , c ) = begin |
| 711 | 435 φ (( id1 Sets (FObj F x) □ φ ) ( ( Iso.≅→ (mα-iso isM) ) ((a , b) , c))) |
| 710 | 436 ≡⟨⟩ |
| 711 | 437 φ ( a , φ (b , c)) |
| 715 | 438 ≡⟨ IsHaskellMonoidalFunctor.assocφ ismf ⟩ |
| 711 | 439 ( FMap F (Iso.≅→ (mα-iso isM))) (φ (( φ (a , b)) , c )) |
| 710 | 440 ≡⟨⟩ |
| 711 | 441 ( FMap F (Iso.≅→ (mα-iso isM))) (φ (( φ □ id1 Sets (FObj F f) ) ((a , b) , c))) |
| 710 | 442 ∎ |
| 443 where | |
| 713 | 444 open Relation.Binary.PropositionalEquality.≡-Reasoning |
| 711 | 445 comm1 : {a b c : Obj Sets} → Sets [ Sets [ φ |
| 446 o Sets [ (id1 Sets (FObj F a) □ φ ) o Iso.≅→ (mα-iso isM) ] ] | |
| 447 ≈ Sets [ FMap F (Iso.≅→ (mα-iso isM)) o Sets [ φ o (φ □ id1 Sets (FObj F c)) ] ] ] | |
| 710 | 448 comm1 {a} {b} {c} = extensionality Sets ( λ x → comm10 x ) |
| 712 | 449 comm20 : {a b : Obj Sets} ( x : FObj F a * One ) → ( Sets [ |
| 450 FMap F (Iso.≅→ (mρ-iso isM)) o Sets [ φ o | |
| 451 FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit )) ] ] ) x ≡ Iso.≅→ (mρ-iso isM) x | |
| 452 comm20 {a} {b} (x , OneObj ) = begin | |
| 453 (FMap F (Iso.≅→ (mρ-iso isM))) ( φ ( x , unit ) ) | |
| 715 | 454 ≡⟨ IsHaskellMonoidalFunctor.idrφ ismf ⟩ |
| 712 | 455 x |
| 456 ≡⟨⟩ | |
| 457 Iso.≅→ (mρ-iso isM) ( x , OneObj ) | |
| 458 ∎ | |
| 459 where | |
| 713 | 460 open Relation.Binary.PropositionalEquality.≡-Reasoning |
| 709 | 461 comm2 : {a b : Obj Sets} → Sets [ Sets [ |
| 711 | 462 FMap F (Iso.≅→ (mρ-iso isM)) o Sets [ φ o |
| 709 | 463 FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit )) ] ] ≈ Iso.≅→ (mρ-iso isM) ] |
| 712 | 464 comm2 {a} {b} = extensionality Sets ( λ x → comm20 {a} {b} x ) |
| 465 comm30 : {a b : Obj Sets} ( x : One * FObj F b ) → ( Sets [ | |
| 466 FMap F (Iso.≅→ (mλ-iso isM)) o Sets [ φ o | |
| 467 FMap (m-bi MonoidalSets) ((λ _ → unit ) , id1 Sets (FObj F b) ) ] ] ) x ≡ Iso.≅→ (mλ-iso isM) x | |
| 468 comm30 {a} {b} ( OneObj , x) = begin | |
| 469 (FMap F (Iso.≅→ (mλ-iso isM))) ( φ ( unit , x ) ) | |
| 715 | 470 ≡⟨ IsHaskellMonoidalFunctor.idlφ ismf ⟩ |
| 712 | 471 x |
| 472 ≡⟨⟩ | |
| 473 Iso.≅→ (mλ-iso isM) ( OneObj , x ) | |
| 474 ∎ | |
| 711 | 475 where |
| 713 | 476 open Relation.Binary.PropositionalEquality.≡-Reasoning |
| 709 | 477 comm3 : {a b : Obj Sets} → Sets [ Sets [ FMap F (Iso.≅→ (mλ-iso isM)) o |
| 711 | 478 Sets [ φ o FMap (m-bi MonoidalSets) ((λ _ → unit ) , id1 Sets (FObj F b)) ] ] ≈ Iso.≅→ (mλ-iso isM) ] |
| 712 | 479 comm3 {a} {b} = extensionality Sets ( λ x → comm30 {a} {b} x ) |
| 709 | 480 |
|
705
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
481 |
| 720 | 482 _・_ : {c₁ : Level} { a b c : Obj (Sets {c₁} ) } → (b → c) → (a → b) → a → c |
| 483 _・_ f g = λ x → f ( g x ) | |
| 713 | 484 |
| 485 record IsApplicative {c₁ : Level} ( f : Functor (Sets {c₁}) (Sets {c₁}) ) | |
| 486 ( pure : {a : Obj Sets} → Hom Sets a ( FObj f a ) ) | |
| 487 ( _<*>_ : {a b : Obj Sets} → FObj f ( a → b ) → FObj f a → FObj f b ) | |
| 488 : Set (suc (suc c₁)) where | |
| 489 field | |
| 714 | 490 -- http://www.staff.city.ac.uk/~ross/papers/Applicative.pdf |
| 713 | 491 identity : { a : Obj Sets } { u : FObj f a } → pure ( id1 Sets a ) <*> u ≡ u |
| 492 composition : { a b c : Obj Sets } { u : FObj f ( b → c ) } { v : FObj f (a → b ) } { w : FObj f a } | |
| 493 → (( pure _・_ <*> u ) <*> v ) <*> w ≡ u <*> (v <*> w) | |
| 494 homomorphism : { a b : Obj Sets } { f : Hom Sets a b } { x : a } → pure f <*> pure x ≡ pure (f x) | |
| 495 interchange : { a b : Obj Sets } { u : FObj f ( a → b ) } { x : a } → u <*> pure x ≡ pure (λ f → f x) <*> u | |
| 496 | |
| 497 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
|
498 : Set (suc (suc c₁)) where |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
499 field |
| 713 | 500 pure : {a : Obj Sets} → Hom Sets a ( FObj F a ) |
| 501 <*> : {a b : Obj Sets} → FObj F ( a → b ) → FObj F a → FObj F b | |
|
707
808b03184fd3
Applicative ⇔ Monoidal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
706
diff
changeset
|
502 -- should have Applicative law |
|
705
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
503 |
| 713 | 504 lemma1 : {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) ) → Applicative F → HaskellMonoidalFunctor F |
| 505 lemma1 F app = record { unit = unit ; φ = φ } | |
|
705
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
506 where |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
507 open Applicative |
| 713 | 508 unit : FObj F One |
| 706 | 509 unit = pure app OneObj |
| 713 | 510 φ : {a b : Obj Sets} → Hom Sets ((FObj F a) * (FObj F b )) ( FObj F ( a * b ) ) |
| 511 φ {a} {b} ( x , y ) = <*> app (FMap F (λ j k → (j , k)) x) y | |
|
705
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
512 |
| 713 | 513 lemma2 : {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) ) → HaskellMonoidalFunctor F → Applicative F |
| 514 lemma2 F mono = record { pure = pure ; <*> = <*> } | |
|
705
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
515 where |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
516 open HaskellMonoidalFunctor |
| 713 | 517 pure : {a : Obj Sets} → Hom Sets a ( FObj F a ) |
| 518 pure {a} x = FMap F ( λ y → x ) (unit mono) | |
| 519 <*> : {a b : Obj Sets} → FObj F ( a → b ) → FObj F a → FObj F b -- ** mono x y | |
| 715 | 520 <*> {a} {b} x y = FMap F ( λ r → ( proj₁ r ) ( proj₂ r ) ) (φ mono ( x , y )) |
| 713 | 521 |
|
719
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
522 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
|
523 → 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
|
524 → 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
|
525 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
|
526 MF = F |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
527 ; ψ = λ x → unit |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
528 ; isMonodailFunctor = record { |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
529 φab = record { TMap = λ x → φ ; isNTrans = record { commute = comm0 } } |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
530 ; associativity = λ {a b c} → comm1 {a} {b} {c} |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
531 ; unitarity-idr = λ {a b} → comm2 {a} {b} |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
532 ; unitarity-idl = λ {a b} → comm3 {a} {b} |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
533 } |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
534 } where |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
535 open Monoidal |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
536 open IsMonoidal hiding ( _■_ ; _□_ ) |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
537 M = MonoidalSets |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
538 isM = Monoidal.isMonoidal MonoidalSets |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
539 unit = Applicative.pure mf OneObj |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
540 _⊗_ : (x y : Obj Sets ) → Obj Sets |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
541 _⊗_ 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
|
542 _□_ : {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
|
543 _□_ 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
|
544 φ : {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
|
545 φ 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
|
546 _<*>_ : {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
|
547 _<*>_ = Applicative.<*> mf |
|
721
a8b595fb4905
use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
548 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
|
549 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
|
550 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
|
551 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
|
552 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
|
553 id x = x |
| 720 | 554 pure : {a : Obj Sets } → Hom Sets a ( FObj F a ) |
| 555 pure a = Applicative.pure mf a | |
| 725 | 556 -- special case |
| 557 F→pureid : {a b : Obj Sets } → (x : FObj F a ) → FMap F id x ≡ pure id <*> x | |
| 558 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
|
559 pure id <*> x |
|
69f01b82dfc9
uniquness of functor fmap
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
721
diff
changeset
|
560 ≡⟨ IsApplicative.identity ismf ⟩ |
|
69f01b82dfc9
uniquness of functor fmap
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
721
diff
changeset
|
561 x |
|
69f01b82dfc9
uniquness of functor fmap
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
721
diff
changeset
|
562 ≡⟨ ≡-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
|
563 ∎ ) |
|
69f01b82dfc9
uniquness of functor fmap
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
721
diff
changeset
|
564 where |
|
69f01b82dfc9
uniquness of functor fmap
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
721
diff
changeset
|
565 open Relation.Binary.PropositionalEquality |
|
69f01b82dfc9
uniquness of functor fmap
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
721
diff
changeset
|
566 open Relation.Binary.PropositionalEquality.≡-Reasoning |
|
723
40122e9c7fc9
postulate Free Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
722
diff
changeset
|
567 ----- |
| 724 | 568 -- they say it not possible prove FreeTheorem in Agda nor Coq |
|
723
40122e9c7fc9
postulate Free Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
722
diff
changeset
|
569 -- https://stackoverflow.com/questions/24718567/is-it-possible-to-get-hold-of-free-theorems-as-propositional-equalities |
|
40122e9c7fc9
postulate Free Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
722
diff
changeset
|
570 -- and we cannot indent postulate ... |
|
40122e9c7fc9
postulate Free Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
722
diff
changeset
|
571 postulate FreeTheorem : {l : Level } {a b c : Obj (Sets {l}) } → (F : Functor (Sets {l}) (Sets {l} ) ) → ( fmap : {a : Obj Sets } {b : Obj Sets } → Hom Sets a b → Hom Sets (FObj F a) ( FObj F b) ) → {h f : Hom Sets a b } → {g k : Hom Sets b c } → Sets [ g o h ≈ k o f ] → Sets [ FMap F g o fmap h ≈ fmap k o FMap F f ] |
|
40122e9c7fc9
postulate Free Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
722
diff
changeset
|
572 UniqunessOfFunctor : (F : Functor Sets Sets) |
|
40122e9c7fc9
postulate Free Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
722
diff
changeset
|
573 {a b : Obj Sets } { f : Hom Sets a b } → ( fmap : {a : Obj Sets } {b : Obj Sets } → Hom Sets a b → Hom Sets (FObj F a) ( FObj F b) ) |
| 724 | 574 → ( {b : Obj Sets } → Sets [ fmap (id1 Sets b) ≈ id1 Sets (FObj F b) ] ) |
|
723
40122e9c7fc9
postulate Free Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
722
diff
changeset
|
575 → Sets [ fmap f ≈ FMap F f ] |
| 724 | 576 UniqunessOfFunctor F {a} {b} {f} fmap eq = begin |
| 577 fmap f | |
| 578 ≈↑⟨ idL ⟩ | |
| 579 id1 Sets (FObj F b) o fmap f | |
| 580 ≈↑⟨ car ( IsFunctor.identity (isFunctor F )) ⟩ | |
| 581 FMap F (id1 Sets b) o fmap f | |
| 582 ≈⟨ FreeTheorem F fmap refl-hom ⟩ | |
| 583 fmap (id1 Sets b) o FMap F f | |
| 584 ≈⟨ car eq ⟩ | |
| 585 id1 Sets (FObj F b) o FMap F f | |
| 586 ≈⟨ idL ⟩ | |
| 587 FMap F f | |
| 588 ∎ | |
| 589 where open ≈-Reasoning Sets hiding ( _o_ ) | |
| 725 | 590 F→pure : {a b : Obj Sets } → { f : a → b } → {x : FObj F a } → FMap F f x ≡ pure f <*> x |
| 591 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
|
592 pure f <*> x |
| 724 | 593 ≡⟨ ≡-cong ( λ k → k x ) (UniqunessOfFunctor 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
|
594 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
|
595 ∎ ) |
|
a8b595fb4905
use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
596 where |
|
a8b595fb4905
use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
597 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
|
598 open Relation.Binary.PropositionalEquality.≡-Reasoning |
| 725 | 599 p*p : { a b : Obj Sets } { f : Hom Sets a b } { x : a } → pure f <*> pure x ≡ pure (f x) |
| 600 p*p = IsApplicative.homomorphism ismf | |
| 601 car : { a b c : Obj Sets } { f : Hom Sets a (b → c) } { x : a } { y : FObj F b } | |
| 602 → ( (pure f <*> pure x ) <*> y ) ≡ ( pure (f x) <*> y ) | |
| 603 car = left ( IsApplicative.homomorphism ismf ) | |
| 604 cdr : { a b c d : Obj Sets } { f : Hom Sets a c } { x : a } { y : FObj F (c → d) } | |
| 605 → y <*> (pure f <*> pure x ) ≡ y <*> ( pure (f x) ) | |
| 606 cdr = right ( IsApplicative.homomorphism ismf ) | |
| 607 cdar : { a b c d : Obj Sets } { f : Hom Sets a (b → c) } { x : a } { y : FObj F b } { y1 : FObj F (c → d) } | |
| 608 → y1 <*> ( (pure f <*> pure x ) <*> y ) ≡ y1 <*> ( pure (f x) <*> y ) | |
| 609 cdar = right ( left ( IsApplicative.homomorphism ismf ) ) | |
| 610 cadr : { a b c d e : Obj Sets } { f : Hom Sets a c } { x : a } { y : FObj F (c → ( e → a )) } { y1 : FObj F e } | |
| 611 → (y <*> (pure f <*> pure x )) <*> y1 ≡ (y <*> ( pure (f x) )) <*> y1 | |
| 612 cadr = left (right ( IsApplicative.homomorphism ismf ) ) | |
| 613 comp = IsApplicative.composition ismf | |
| 614 inter = IsApplicative.interchange ismf | |
|
719
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
615 comm00 : {a b : Obj (Sets × Sets)} { f : Hom (Sets × Sets) a b} (x : ( FObj F (proj₁ a) * FObj F (proj₂ a)) ) → |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
616 (Sets [ FMap (Functor⊗ Sets Sets MonoidalSets F) f o φ ]) x ≡ (Sets [ φ o FMap (Functor● Sets Sets MonoidalSets F) f ]) x |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
617 comm00 {a} {b} {(f , g)} (x , y) = begin |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
618 ( 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
|
619 ≡⟨⟩ |
| 725 | 620 FMap F (λ xy → f (proj₁ xy) , g (proj₂ xy)) ((FMap F (λ j k → j , k) x) <*> y) |
| 621 ≡⟨⟩ | |
|
721
a8b595fb4905
use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
622 FMap F (map f g) ((FMap F (λ j k → j , k) x) <*> y) |
| 725 | 623 ≡⟨ F→pure ⟩ |
| 624 (pure (map f g) <*> (FMap F (λ j k → j , k) x <*> y)) | |
| 625 ≡⟨ 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
|
626 (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
|
627 ≡⟨ 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
|
628 (( 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
|
629 ≡⟨ 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
|
630 ((( pure _・_ <*> (( pure _・_ <*> (pure (map f g))))) <*> pure (λ j k → j , k)) <*> x) <*> y |
| 725 | 631 ≡⟨ 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
|
632 (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
|
633 ≡⟨⟩ |
|
a8b595fb4905
use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
634 (pure (λ j k → f j , g k) <*> x) <*> y |
| 725 | 635 ≡⟨⟩ |
|
721
a8b595fb4905
use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
636 ( pure ((_・_ (( _・_ ( ( λ h → h g ))) ( _・_ ))) ((λ j k → f j , k))) <*> x ) <*> y |
| 725 | 637 ≡⟨ sym ( trans (left (left (left p*p))) (left ( left p*p)) ) ⟩ |
| 638 ((((pure _・_ <*> pure ((λ h → h g) ・ _・_)) <*> pure (λ j k → f j , k)) <*> x) <*> y) | |
| 639 ≡⟨ 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
|
640 (((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
|
641 ≡⟨ 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
|
642 ((( 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
|
643 ≡⟨ 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
|
644 ( 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
|
645 ≡⟨ 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
|
646 (( 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
|
647 ≡⟨ IsApplicative.composition ismf ⟩ |
|
a8b595fb4905
use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
648 (pure (λ j k → f j , k) <*> x) <*> (pure g <*> y) |
| 725 | 649 ≡⟨ 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
|
650 (FMap F (λ j k → f j , k) x) <*> (FMap F g y) |
| 720 | 651 ≡⟨ ≡-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
|
652 (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
|
653 ≡⟨⟩ |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
654 φ ( ( 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
|
655 ∎ |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
656 where |
|
721
a8b595fb4905
use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
657 open Relation.Binary.PropositionalEquality |
|
719
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
658 open Relation.Binary.PropositionalEquality.≡-Reasoning |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
659 comm0 : {a b : Obj (Sets × Sets)} { f : Hom (Sets × Sets) a b} → Sets [ Sets [ FMap (Functor⊗ Sets Sets MonoidalSets F) f o φ ] |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
660 ≈ Sets [ φ o FMap (Functor● Sets Sets MonoidalSets F) f ] ] |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
661 comm0 {a} {b} {f} = extensionality Sets ( λ (x : ( FObj F (proj₁ a) * FObj F (proj₂ a)) ) → comm00 x ) |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
662 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 ≡ |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
663 (Sets [ FMap F (Iso.≅→ (mα-iso isM)) o Sets [ φ o φ □ id1 Sets (FObj F c) ] ]) x |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
664 comm10 {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
|
665 φ (( id □ φ ) ( ( Iso.≅→ (mα-iso isM) ) ((a , b) , c))) |
| 720 | 666 ≡⟨⟩ |
| 667 (FMap F (λ j k → j , k) a) <*> ( (FMap F (λ j k → j , k) b) <*> c) | |
| 726 | 668 ≡⟨ trans (left F→pure) (right (left F→pure) ) ⟩ |
| 725 | 669 (pure (λ j k → j , k) <*> a) <*> ( (pure (λ j k → j , k) <*> b) <*> c) |
| 726 | 670 ≡⟨ sym comp ⟩ |
| 725 | 671 ( ( pure _・_ <*> (pure (λ j k → j , k) <*> a)) <*> (pure (λ j k → j , k) <*> b)) <*> c |
| 726 | 672 ≡⟨ sym ( left comp ) ⟩ |
| 725 | 673 (( ( pure _・_ <*> ( pure _・_ <*> (pure (λ j k → j , k) <*> a))) <*> (pure (λ j k → j , k))) <*> b) <*> c |
| 726 | 674 ≡⟨ sym ( left ( left ( left (right comp )))) ⟩ |
| 725 | 675 (( ( pure _・_ <*> (( (pure _・_ <*> pure _・_ ) <*> (pure (λ j k → j , k))) <*> a)) <*> (pure (λ j k → j , k))) <*> b) <*> c |
| 726 | 676 ≡⟨ trans (left ( left (left ( right (left ( left p*p )))))) (left ( left ( left (right (left p*p))))) ⟩ |
| 725 | 677 (( ( pure _・_ <*> ((pure ((_・_ ( _・_ )) ((λ j k → j , k)))) <*> a)) <*> (pure (λ j k → j , k))) <*> b) <*> c |
| 726 | 678 ≡⟨ sym (left ( left ( left comp ) )) ⟩ |
| 725 | 679 (((( ( pure _・_ <*> (pure _・_ )) <*> (pure ((_・_ ( _・_ )) ((λ j k → j , k))))) <*> a) <*> (pure (λ j k → j , k))) <*> b) <*> c |
| 726 | 680 ≡⟨ trans (left ( left ( left (left (left p*p))))) (left ( left ( left (left p*p )))) ⟩ |
| 725 | 681 ((((pure ( ( _・_ (_・_ )) (((_・_ ( _・_ )) ((λ j k → j , k)))))) <*> a) <*> (pure (λ j k → j , k))) <*> b) <*> c |
| 682 ≡⟨⟩ | |
| 683 ((((pure (λ f g x y → f , g x y)) <*> a) <*> (pure (λ j k → j , k))) <*> b) <*> c | |
| 726 | 684 ≡⟨ left ( left inter ) ⟩ |
| 725 | 685 (((pure (λ f → f (λ j k → j , k))) <*> ((pure (λ f g x y → f , g x y)) <*> a) ) <*> b) <*> c |
| 726 | 686 ≡⟨ sym ( left ( left comp )) ⟩ |
| 725 | 687 (((( pure _・_ <*> (pure (λ f → f (λ j k → j , k)))) <*> (pure (λ f g x y → f , g x y))) <*> a ) <*> b) <*> c |
| 726 | 688 ≡⟨ trans (left ( left (left (left p*p) ))) (left (left (left p*p ) )) ⟩ |
| 725 | 689 ((pure (( _・_ (λ f → f (λ j k → j , k))) (λ f g x y → f , g x y)) <*> a ) <*> b) <*> c |
| 690 ≡⟨⟩ | |
| 691 (((pure (λ f g h → f , g , h)) <*> a) <*> b) <*> c | |
| 692 ≡⟨⟩ | |
| 693 ((pure ((_・_ ((_・_ ((_・_ ( (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc))))))) | |
| 694 (( _・_ ( _・_ ((λ j k → j , k)))) (λ j k → j , k))) <*> a) <*> b) <*> c | |
| 726 | 695 ≡⟨ sym (trans ( left ( left ( left (left (right (right p*p))) ) )) (trans (left (left( left (left (right p*p))))) |
| 696 (trans (left (left (left (left p*p)))) (trans ( left (left (left (right (left (right p*p )))))) | |
| 697 (trans (left (left (left (right (left p*p))))) (trans (left (left (left (right p*p)))) (left (left (left p*p)))) ) ) ) | |
| 698 ) ) ⟩ | |
| 725 | 699 ((((pure _・_ <*> ((pure _・_ <*> ((pure _・_ <*> ( pure (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc))))))) <*> |
| 700 (( pure _・_ <*> ( pure _・_ <*> (pure (λ j k → j , k)))) <*> pure (λ j k → j , k))) <*> a) <*> b) <*> c | |
| 726 | 701 ≡⟨ left (left comp ) ⟩ |
| 725 | 702 (((pure _・_ <*> ((pure _・_ <*> ( pure (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc))))) <*> |
| 703 ((( pure _・_ <*> ( pure _・_ <*> (pure (λ j k → j , k)))) <*> pure (λ j k → j , k)) <*> a)) <*> b) <*> c | |
| 726 | 704 ≡⟨ left comp ⟩ |
| 725 | 705 ((pure _・_ <*> ( pure (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc))) <*> |
| 706 (((( pure _・_ <*> ( pure _・_ <*> (pure (λ j k → j , k)))) <*> pure (λ j k → j , k)) <*> a) <*> b)) <*> c | |
| 726 | 707 ≡⟨ left ( right (left comp )) ⟩ |
| 725 | 708 ((pure _・_ <*> ( pure (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc))) <*> |
| 709 ((( pure _・_ <*> (pure (λ j k → j , k))) <*> (pure (λ j k → j , k) <*> a)) <*> b)) <*> c | |
| 726 | 710 ≡⟨ left ( right comp ) ⟩ |
| 725 | 711 ((pure _・_ <*> ( pure (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc))) <*> |
| 712 (pure (λ j k → j , k) <*> ( (pure (λ j k → j , k) <*> a) <*> b))) <*> c | |
| 726 | 713 ≡⟨ comp ⟩ |
| 725 | 714 pure (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc) <*> ( (pure (λ j k → j , k) <*> ( (pure (λ j k → j , k) <*> a) <*> b)) <*> c) |
| 726 | 715 ≡⟨ sym ( trans ( trans F→pure (right (left F→pure ))) ( right ( left (right (left F→pure ))))) ⟩ |
| 720 | 716 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) |
| 717 ≡⟨⟩ | |
| 718 ( 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
|
719 ∎ |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
720 where |
| 720 | 721 open Relation.Binary.PropositionalEquality |
|
719
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
722 open Relation.Binary.PropositionalEquality.≡-Reasoning |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
723 comm1 : {a b c : Obj Sets} → Sets [ Sets [ φ |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
724 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
|
725 ≈ Sets [ FMap F (Iso.≅→ (mα-iso isM)) o Sets [ φ o (φ □ id1 Sets (FObj F c)) ] ] ] |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
726 comm1 {a} {b} {c} = extensionality Sets ( λ x → comm10 x ) |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
727 comm20 : {a b : Obj Sets} ( x : FObj F a * One ) → ( Sets [ |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
728 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
|
729 FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit )) ] ] ) x ≡ Iso.≅→ (mρ-iso isM) x |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
730 comm20 {a} {b} (x , OneObj ) = begin |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
731 (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
|
732 ≡⟨⟩ |
| 720 | 733 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
|
734 ≡⟨ ≡-cong ( λ k → FMap F proj₁ k) ( IsApplicative.interchange ismf ) ⟩ |
| 720 | 735 FMap F proj₁ ((pure (λ f → f OneObj)) <*> (FMap F (λ j k → j , k) x)) |
| 725 | 736 ≡⟨ ( trans F→pure (right ( right F→pure )) ) ⟩ |
| 737 pure proj₁ <*> ((pure (λ f → f OneObj)) <*> (pure (λ j k → j , k) <*> x)) | |
| 738 ≡⟨ sym ( right comp ) ⟩ | |
| 739 pure proj₁ <*> (((pure _・_ <*> (pure (λ f → f OneObj))) <*> pure (λ j k → j , k)) <*> x) | |
| 740 ≡⟨ sym comp ⟩ | |
| 741 ( ( pure _・_ <*> (pure proj₁ ) ) <*> ((pure _・_ <*> (pure (λ f → f OneObj))) <*> pure (λ j k → j , k))) <*> x | |
| 742 ≡⟨ 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
|
743 pure ( ( _・_ (proj₁ {l} {l})) ((_・_ ((λ f → f OneObj))) (λ j k → j , k))) <*> x |
| 725 | 744 ≡⟨⟩ |
| 745 pure id <*> x | |
| 746 ≡⟨ IsApplicative.identity ismf ⟩ | |
|
719
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
747 x |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
748 ≡⟨⟩ |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
749 Iso.≅→ (mρ-iso isM) (x , OneObj) |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
750 ∎ |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
751 where |
| 725 | 752 open Relation.Binary.PropositionalEquality |
|
719
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
753 open Relation.Binary.PropositionalEquality.≡-Reasoning |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
754 comm2 : {a b : Obj Sets} → Sets [ Sets [ |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
755 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
|
756 FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit )) ] ] ≈ Iso.≅→ (mρ-iso isM) ] |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
757 comm2 {a} {b} = extensionality Sets ( λ x → comm20 {a} {b} x ) |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
758 comm30 : {a b : Obj Sets} ( x : One * FObj F b ) → ( Sets [ |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
759 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
|
760 FMap (m-bi MonoidalSets) ((λ _ → unit ) , id1 Sets (FObj F b) ) ] ] ) x ≡ Iso.≅→ (mλ-iso isM) x |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
761 comm30 {a} {b} ( OneObj , x) = begin |
| 720 | 762 (FMap F (Iso.≅→ (mλ-iso isM))) ( φ ( unit , x ) ) |
| 763 ≡⟨⟩ | |
| 764 FMap F proj₂ ((FMap F (λ j k → j , k) (pure OneObj)) <*> x) | |
| 725 | 765 ≡⟨ ( trans F→pure (right ( left F→pure )) ) ⟩ |
| 766 pure proj₂ <*> ((pure (λ j k → j , k) <*> (pure OneObj)) <*> x) | |
| 767 ≡⟨ sym comp ⟩ | |
| 768 ((pure _・_ <*> (pure proj₂)) <*> (pure (λ j k → j , k) <*> (pure OneObj))) <*> x | |
| 769 ≡⟨ 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
|
770 pure ((_・_ (proj₂ {l}) )((λ (j : One {l}) (k : b ) → j , k) OneObj)) <*> x |
| 725 | 771 ≡⟨⟩ |
| 772 pure id <*> x | |
| 773 ≡⟨ IsApplicative.identity ismf ⟩ | |
| 720 | 774 x |
| 775 ≡⟨⟩ | |
| 776 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
|
777 ∎ |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
778 where |
| 725 | 779 open Relation.Binary.PropositionalEquality |
|
719
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
780 open Relation.Binary.PropositionalEquality.≡-Reasoning |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
781 comm3 : {a b : Obj Sets} → Sets [ Sets [ FMap F (Iso.≅→ (mλ-iso isM)) o |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
782 Sets [ φ o FMap (m-bi MonoidalSets) ((λ _ → unit ) , id1 Sets (FObj F b)) ] ] ≈ Iso.≅→ (mλ-iso isM) ] |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
783 comm3 {a} {b} = extensionality Sets ( λ x → comm30 {a} {b} x ) |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
784 |
|
a017ed40dd77
Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
717
diff
changeset
|
785 |
| 713 | 786 |
| 787 HaskellMonoidal→Applicative : {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) ) | |
| 788 ( unit : FObj F One ) | |
| 789 ( φ : {a b : Obj Sets} → Hom Sets ((FObj F a) * (FObj F b )) ( FObj F ( a * b ) ) ) | |
| 790 ( mono : IsHaskellMonoidalFunctor F unit φ ) | |
| 715 | 791 → IsApplicative F (λ x → FMap F ( λ y → x ) unit) (λ x y → FMap F ( λ r → ( proj₁ r ) ( proj₂ r ) ) (φ ( x , y ))) |
| 713 | 792 HaskellMonoidal→Applicative {c₁} F unit φ mono = record { |
| 793 identity = identity | |
| 794 ; composition = composition | |
| 795 ; homomorphism = homomorphism | |
| 796 ; interchange = interchange | |
| 797 } | |
| 798 where | |
| 714 | 799 id : { a : Obj Sets } → a → a |
| 800 id x = x | |
| 713 | 801 isM : IsMonoidal (Sets {c₁}) One SetsTensorProduct |
| 802 isM = Monoidal.isMonoidal MonoidalSets | |
| 803 pure : {a : Obj Sets} → Hom Sets a ( FObj F a ) | |
| 804 pure {a} x = FMap F ( λ y → x ) (unit ) | |
| 805 _<*>_ : {a b : Obj Sets} → FObj F ( a → b ) → FObj F a → FObj F b | |
| 715 | 806 _<*>_ {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
|
807 -- 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
|
808 -- 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
|
809 -- 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
|
810 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
|
811 left {_} {_} {_} {_} {_} {h} eq = ≡-cong ( λ k → k h ) eq |
| 715 | 812 open Relation.Binary.PropositionalEquality |
|
717
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
813 FφF→F : { a b c d e : Obj Sets } { g : Hom Sets a c } { h : Hom Sets b d } |
| 715 | 814 { f : Hom Sets (c * d) e } |
| 815 { x : FObj F a } { y : FObj F b } | |
| 816 → 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
|
817 FφF→F {a} {b} {c} {d} {e} {g} {h} {f} {x} {y} = sym ( begin |
| 715 | 818 FMap F ( f o map g h ) ( φ ( x , y ) ) |
| 819 ≡⟨ ≡-cong ( λ k → k ( φ ( x , y ))) ( IsFunctor.distr (isFunctor F) ) ⟩ | |
| 820 FMap F f (( FMap F ( map g h ) ) ( φ ( x , y ))) | |
| 821 ≡⟨ ≡-cong ( λ k → FMap F f k ) ( IsHaskellMonoidalFunctor.natφ mono ) ⟩ | |
| 822 FMap F f ( φ ( FMap F g x , FMap F h y ) ) | |
| 823 ∎ ) | |
| 824 where | |
| 825 open Relation.Binary.PropositionalEquality.≡-Reasoning | |
| 716 | 826 u→F : {a : Obj Sets } {u : FObj F a} → u ≡ FMap F id u |
| 827 u→F {a} {u} = sym ( ≡-cong ( λ k → k u ) ( IsFunctor.identity ( isFunctor F ) ) ) | |
| 828 φunitr : {a : Obj Sets } {u : FObj F a} → φ ( unit , u) ≡ FMap F (Iso.≅← (IsMonoidal.mλ-iso isM)) u | |
| 829 φunitr {a} {u} = sym ( begin | |
| 830 FMap F (Iso.≅← (IsMonoidal.mλ-iso isM)) u | |
| 831 ≡⟨ ≡-cong ( λ k → FMap F (Iso.≅← (IsMonoidal.mλ-iso isM)) k ) (sym (IsHaskellMonoidalFunctor.idlφ mono)) ⟩ | |
| 832 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
|
833 ≡⟨ left ( sym ( IsFunctor.distr ( isFunctor F ) )) ⟩ |
| 716 | 834 (FMap F ( (Iso.≅← (IsMonoidal.mλ-iso isM)) o (Iso.≅→ (IsMonoidal.mλ-iso isM)))) ( φ ( unit , u) ) |
| 835 ≡⟨ ≡-cong ( λ k → FMap F k ( φ ( unit , u) )) (Iso.iso→ ( (IsMonoidal.mλ-iso isM) )) ⟩ | |
| 836 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
|
837 ≡⟨ left ( IsFunctor.identity ( isFunctor F ) ) ⟩ |
| 716 | 838 id ( φ ( unit , u) ) |
| 839 ≡⟨⟩ | |
| 840 φ ( unit , u) | |
| 841 ∎ ) | |
| 842 where | |
| 843 open Relation.Binary.PropositionalEquality.≡-Reasoning | |
| 844 φunitl : {a : Obj Sets } {u : FObj F a} → φ ( u , unit ) ≡ FMap F (Iso.≅← (IsMonoidal.mρ-iso isM)) u | |
| 845 φunitl {a} {u} = sym ( begin | |
| 846 FMap F (Iso.≅← (IsMonoidal.mρ-iso isM)) u | |
| 847 ≡⟨ ≡-cong ( λ k → FMap F (Iso.≅← (IsMonoidal.mρ-iso isM)) k ) (sym (IsHaskellMonoidalFunctor.idrφ mono)) ⟩ | |
| 848 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
|
849 ≡⟨ left ( sym ( IsFunctor.distr ( isFunctor F ) )) ⟩ |
| 716 | 850 (FMap F ( (Iso.≅← (IsMonoidal.mρ-iso isM)) o (Iso.≅→ (IsMonoidal.mρ-iso isM)))) ( φ ( u , unit ) ) |
| 851 ≡⟨ ≡-cong ( λ k → FMap F k ( φ ( u , unit ) )) (Iso.iso→ ( (IsMonoidal.mρ-iso isM) )) ⟩ | |
| 852 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
|
853 ≡⟨ left ( IsFunctor.identity ( isFunctor F ) ) ⟩ |
| 716 | 854 id ( φ ( u , unit ) ) |
| 855 ≡⟨⟩ | |
| 856 φ ( u , unit ) | |
| 857 ∎ ) | |
| 858 where | |
| 859 open Relation.Binary.PropositionalEquality.≡-Reasoning | |
| 715 | 860 open IsMonoidal |
| 713 | 861 identity : { a : Obj Sets } { u : FObj F a } → pure ( id1 Sets a ) <*> u ≡ u |
| 862 identity {a} {u} = begin | |
| 714 | 863 pure id <*> u |
| 713 | 864 ≡⟨⟩ |
| 715 | 865 ( FMap F ( λ r → ( proj₁ r ) ( proj₂ r )) ) ( φ ( FMap F ( λ y → id ) unit , u ) ) |
| 716 | 866 ≡⟨ ≡-cong ( λ k → ( FMap F ( λ r → ( proj₁ r ) ( proj₂ r )) ) ( φ ( FMap F ( λ y → id ) unit , k ))) u→F ⟩ |
| 715 | 867 ( 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
|
868 ≡⟨ FφF→F ⟩ |
| 713 | 869 FMap F (λ x → proj₂ x ) (φ (unit , u ) ) |
| 870 ≡⟨⟩ | |
| 871 FMap F (Iso.≅→ (mλ-iso isM)) (φ (unit , u )) | |
| 715 | 872 ≡⟨ IsHaskellMonoidalFunctor.idlφ mono ⟩ |
| 713 | 873 u |
| 874 ∎ | |
| 875 where | |
| 876 open Relation.Binary.PropositionalEquality.≡-Reasoning | |
| 877 composition : { a b c : Obj Sets } { u : FObj F ( b → c ) } { v : FObj F (a → b ) } { w : FObj F a } | |
| 878 → (( pure _・_ <*> u ) <*> v ) <*> w ≡ u <*> (v <*> w) | |
| 879 composition {a} {b} {c} {u} {v} {w} = begin | |
| 715 | 880 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ |
| 881 (FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ y f g x → f (g x)) unit , u)) , v)) , w)) | |
| 716 | 882 ≡⟨ ≡-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 | 883 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ |
| 716 | 884 (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
|
885 ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ ( k , v)) , w)) ) FφF→F ⟩ |
| 715 | 886 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ |
| 716 | 887 (FMap F ( λ x → (λ r → proj₁ r (proj₂ r)) ((map (λ y f g x → f (g x)) id ) x)) (φ ( unit , u)) , v)) , w)) |
| 888 ≡⟨ ≡-cong ( λ k → ( FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ | |
| 889 (FMap F ( λ x → (λ r → proj₁ r (proj₂ r)) ((map (λ y f g x → f (g x)) id ) x)) k , v)) , w)) ) ) φunitr ⟩ | |
| 715 | 890 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ |
| 716 | 891 ( (FMap F ( λ x → (λ r → proj₁ r (proj₂ r)) ((map (λ y f g x → f (g x)) id ) x)) (FMap F (Iso.≅← (mλ-iso isM)) u) ) , v)) , w)) |
| 892 ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ | |
| 893 (k u , v)) , w)) ) (sym ( IsFunctor.distr (isFunctor F ))) ⟩ | |
| 894 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ | |
| 895 ( FMap F (λ x → ((λ y f g x₁ → f (g x₁)) unit x) ) u , v)) , w)) | |
| 714 | 896 ≡⟨⟩ |
| 715 | 897 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ |
| 716 | 898 ( FMap F (λ x g h → x (g h) ) u , v)) , w)) |
| 899 ≡⟨ ≡-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 ⟩ | |
| 900 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
|
901 ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (k , w)) ) FφF→F ⟩ |
| 716 | 902 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 | 903 ≡⟨⟩ |
| 716 | 904 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ x h → proj₁ x (proj₂ x h)) (φ (u , v)) , w)) |
| 905 ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ x h → proj₁ x (proj₂ x h)) (φ (u , v)) , k)) ) u→F ⟩ | |
| 906 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
|
907 ≡⟨ FφF→F ⟩ |
| 716 | 908 FMap F ((λ r → proj₁ r (proj₂ r)) o map (λ x h → proj₁ x (proj₂ x h)) id) (φ (φ (u , v) , w)) |
| 714 | 909 ≡⟨⟩ |
| 716 | 910 FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (φ (φ (u , v) , w)) |
| 911 ≡⟨ ≡-cong ( λ k → FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (k (φ (φ (u , v) , w)) )) (sym (IsFunctor.identity (isFunctor F ))) ⟩ | |
| 912 FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (FMap F id (φ (φ (u , v) , w)) ) | |
| 913 ≡⟨ ≡-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))) ⟩ | |
| 914 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)) ) | |
| 915 ≡⟨ ≡-cong ( λ k → FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (k (φ (φ (u , v) , w)))) ( IsFunctor.distr (isFunctor F )) ⟩ | |
| 916 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)) )) | |
| 917 ≡⟨ ≡-cong ( λ k → FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (FMap F (Iso.≅← (mα-iso isM)) k) ) (sym ( IsHaskellMonoidalFunctor.assocφ mono ) ) ⟩ | |
| 918 FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (FMap F (Iso.≅← (mα-iso isM)) (φ (u , φ (v , w)))) | |
| 715 | 919 ≡⟨⟩ |
| 716 | 920 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
|
921 ≡⟨ left (sym ( IsFunctor.distr (isFunctor F ))) ⟩ |
| 716 | 922 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 | 923 ≡⟨⟩ |
| 716 | 924 FMap F (λ y → proj₁ y (proj₁ (proj₂ y) (proj₂ (proj₂ y)))) (φ (u , φ (v , w))) |
| 715 | 925 ≡⟨⟩ |
| 926 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
|
927 ≡⟨ sym FφF→F ⟩ |
| 715 | 928 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F id u , FMap F (λ r → proj₁ r (proj₂ r)) (φ (v , w)))) |
| 716 | 929 ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (k , FMap F (λ r → proj₁ r (proj₂ r)) (φ (v , w)))) ) (sym u→F ) ⟩ |
| 715 | 930 FMap F (λ r → proj₁ r (proj₂ r)) (φ (u , FMap F (λ r → proj₁ r (proj₂ r)) (φ (v , w)))) |
| 713 | 931 ∎ |
| 932 where | |
| 933 open Relation.Binary.PropositionalEquality.≡-Reasoning | |
| 934 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
|
935 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
|
936 pure f <*> pure x |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
937 ≡⟨⟩ |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
938 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
|
939 ≡⟨ FφF→F ⟩ |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
940 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
|
941 ≡⟨⟩ |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
942 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
|
943 ≡⟨ ≡-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
|
944 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
|
945 ≡⟨⟩ |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
946 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
|
947 ≡⟨ 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
|
948 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
|
949 ≡⟨⟩ |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
950 pure (f x) |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
951 ∎ |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
952 where |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
953 open Relation.Binary.PropositionalEquality.≡-Reasoning |
| 713 | 954 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
|
955 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
|
956 u <*> pure x |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
957 ≡⟨⟩ |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
958 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
|
959 ≡⟨ ≡-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
|
960 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
|
961 ≡⟨ FφF→F ⟩ |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
962 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
|
963 ≡⟨⟩ |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
964 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
|
965 ≡⟨ ≡-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
|
966 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
|
967 ≡⟨ 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
|
968 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
|
969 ≡⟨⟩ |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
970 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
|
971 ≡⟨ 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
|
972 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
|
973 ≡⟨ ≡-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
|
974 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
|
975 ≡⟨⟩ |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
976 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
|
977 ≡⟨ sym FφF→F ⟩ |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
978 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
|
979 ≡⟨ ≡-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
|
980 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
|
981 ≡⟨⟩ |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
982 pure (λ f → f x) <*> u |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
983 ∎ |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
984 where |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
985 open Relation.Binary.PropositionalEquality.≡-Reasoning |
|
a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
716
diff
changeset
|
986 |