Mercurial > hg > Members > kono > Proof > category
annotate monoidal.agda @ 713:5e101ee6dab9
identity done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 23 Nov 2017 18:24:44 +0900 |
| parents | 9092874a0633 |
| children | bc21e89cd273 |
| 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}) | |
| 320 MonoidalSets = record { | |
| 321 m-i = One ; | |
| 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 | |
| 366 law1 : { a b c d : Obj Sets } { x : FObj F a} { y : FObj F b} { f : a → c } { g : b → d } | |
| 367 → FMap F (map f g) (φ (x , y)) ≡ φ (FMap F f x , FMap F g y) | |
| 368 law2 : { x y z : Obj Sets } { a : FObj F x } { b : FObj F y }{ c : FObj F z } | |
| 369 → φ (a , φ (b , c)) ≡ FMap F (Iso.≅→ (mα-iso isM)) (φ (φ (a , b) , c)) | |
| 370 law3 : {a : Obj Sets } { x : FObj F a } → FMap F (Iso.≅→ (mρ-iso isM)) (φ (x , unit)) ≡ x | |
| 371 law4 : {a : Obj Sets } { x : FObj F a } → FMap F (Iso.≅→ (mλ-iso isM)) (φ (unit , x)) ≡ x | |
| 372 | |
|
705
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
373 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
|
374 : Set (suc (suc c₁)) where |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
375 field |
| 706 | 376 unit : FObj f One |
|
705
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
377 φ : {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
|
378 ** : {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
|
379 ** x y = φ ( x , y ) |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
380 |
| 713 | 381 lemma0 : {c : Level} ( F : Functor (Sets {c}) (Sets {c}) ) → (mf : HaskellMonoidalFunctor F ) |
| 382 → IsHaskellMonoidalFunctor F ( HaskellMonoidalFunctor.unit mf ) ( HaskellMonoidalFunctor.φ mf ) | |
| 383 → MonoidalFunctor {_} {c} {_} {Sets} {Sets} MonoidalSets MonoidalSets | |
| 384 lemma0 F mf ismf = record { | |
| 709 | 385 MF = F |
| 386 ; ψ = λ _ → HaskellMonoidalFunctor.unit mf | |
| 387 ; isMonodailFunctor = record { | |
| 711 | 388 φab = record { TMap = λ x → φ ; isNTrans = record { commute = comm0 } } |
| 389 ; associativity = λ {a b c} → comm1 {a} {b} {c} | |
| 710 | 390 ; unitarity-idr = λ {a b} → comm2 {a} {b} |
| 391 ; unitarity-idl = λ {a b} → comm3 {a} {b} | |
| 709 | 392 } |
| 393 } where | |
| 394 open Monoidal | |
| 395 open IsMonoidal hiding ( _■_ ; _□_ ) | |
| 396 M = MonoidalSets | |
| 397 isM = Monoidal.isMonoidal MonoidalSets | |
| 398 unit = HaskellMonoidalFunctor.unit mf | |
| 399 _⊗_ : (x y : Obj Sets ) → Obj Sets | |
| 400 _⊗_ x y = (IsMonoidal._□_ (Monoidal.isMonoidal M) ) x y | |
| 401 _□_ : {a b c d : Obj Sets } ( f : Hom Sets a c ) ( g : Hom Sets b d ) → Hom Sets ( a ⊗ b ) ( c ⊗ d ) | |
| 402 _□_ f g = FMap (m-bi M) ( f , g ) | |
| 711 | 403 φ : {x : Obj (Sets × Sets) } → Hom Sets (FObj (Functor● Sets Sets MonoidalSets F) x) (FObj (Functor⊗ Sets Sets MonoidalSets F) x) |
| 404 φ z = HaskellMonoidalFunctor.φ mf z | |
| 710 | 405 comm00 : {a b : Obj (Sets × Sets)} { f : Hom (Sets × Sets) a b} (x : ( FObj F (proj₁ a) * FObj F (proj₂ a)) ) → |
| 711 | 406 (Sets [ FMap (Functor⊗ Sets Sets MonoidalSets F) f o φ ]) x ≡ (Sets [ φ o FMap (Functor● Sets Sets MonoidalSets F) f ]) x |
| 710 | 407 comm00 {a} {b} {(f , g)} (x , y) = begin |
| 711 | 408 (FMap (Functor⊗ Sets Sets MonoidalSets F) (f , g) ) (φ (x , y)) |
| 710 | 409 ≡⟨⟩ |
| 711 | 410 (FMap F ( f □ g ) ) (φ (x , y)) |
| 710 | 411 ≡⟨⟩ |
| 711 | 412 FMap F ( map f g ) (φ (x , y)) |
| 713 | 413 ≡⟨ IsHaskellMonoidalFunctor.law1 ismf ⟩ |
| 711 | 414 φ ( FMap F f x , FMap F g y ) |
| 710 | 415 ≡⟨⟩ |
| 711 | 416 φ ( ( FMap F f □ FMap F g ) (x , y) ) |
| 710 | 417 ≡⟨⟩ |
| 711 | 418 φ ((FMap (Functor● Sets Sets MonoidalSets F) (f , g) ) (x , y) ) |
| 710 | 419 ∎ |
| 420 where | |
| 713 | 421 open Relation.Binary.PropositionalEquality.≡-Reasoning |
| 711 | 422 comm0 : {a b : Obj (Sets × Sets)} { f : Hom (Sets × Sets) a b} → Sets [ Sets [ FMap (Functor⊗ Sets Sets MonoidalSets F) f o φ ] |
| 423 ≈ Sets [ φ o FMap (Functor● Sets Sets MonoidalSets F) f ] ] | |
| 710 | 424 comm0 {a} {b} {f} = extensionality Sets ( λ (x : ( FObj F (proj₁ a) * FObj F (proj₂ a)) ) → comm00 x ) |
| 711 | 425 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 ≡ |
| 426 (Sets [ FMap F (Iso.≅→ (mα-iso isM)) o Sets [ φ o φ □ id1 Sets (FObj F c) ] ]) x | |
| 710 | 427 comm10 {x} {y} {f} ((a , b) , c ) = begin |
| 711 | 428 φ (( id1 Sets (FObj F x) □ φ ) ( ( Iso.≅→ (mα-iso isM) ) ((a , b) , c))) |
| 710 | 429 ≡⟨⟩ |
| 711 | 430 φ ( a , φ (b , c)) |
| 713 | 431 ≡⟨ IsHaskellMonoidalFunctor.law2 ismf ⟩ |
| 711 | 432 ( FMap F (Iso.≅→ (mα-iso isM))) (φ (( φ (a , b)) , c )) |
| 710 | 433 ≡⟨⟩ |
| 711 | 434 ( FMap F (Iso.≅→ (mα-iso isM))) (φ (( φ □ id1 Sets (FObj F f) ) ((a , b) , c))) |
| 710 | 435 ∎ |
| 436 where | |
| 713 | 437 open Relation.Binary.PropositionalEquality.≡-Reasoning |
| 711 | 438 comm1 : {a b c : Obj Sets} → Sets [ Sets [ φ |
| 439 o Sets [ (id1 Sets (FObj F a) □ φ ) o Iso.≅→ (mα-iso isM) ] ] | |
| 440 ≈ Sets [ FMap F (Iso.≅→ (mα-iso isM)) o Sets [ φ o (φ □ id1 Sets (FObj F c)) ] ] ] | |
| 710 | 441 comm1 {a} {b} {c} = extensionality Sets ( λ x → comm10 x ) |
| 712 | 442 comm20 : {a b : Obj Sets} ( x : FObj F a * One ) → ( Sets [ |
| 443 FMap F (Iso.≅→ (mρ-iso isM)) o Sets [ φ o | |
| 444 FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit )) ] ] ) x ≡ Iso.≅→ (mρ-iso isM) x | |
| 445 comm20 {a} {b} (x , OneObj ) = begin | |
| 446 (FMap F (Iso.≅→ (mρ-iso isM))) ( φ ( x , unit ) ) | |
| 713 | 447 ≡⟨ IsHaskellMonoidalFunctor.law3 ismf ⟩ |
| 712 | 448 x |
| 449 ≡⟨⟩ | |
| 450 Iso.≅→ (mρ-iso isM) ( x , OneObj ) | |
| 451 ∎ | |
| 452 where | |
| 713 | 453 open Relation.Binary.PropositionalEquality.≡-Reasoning |
| 709 | 454 comm2 : {a b : Obj Sets} → Sets [ Sets [ |
| 711 | 455 FMap F (Iso.≅→ (mρ-iso isM)) o Sets [ φ o |
| 709 | 456 FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit )) ] ] ≈ Iso.≅→ (mρ-iso isM) ] |
| 712 | 457 comm2 {a} {b} = extensionality Sets ( λ x → comm20 {a} {b} x ) |
| 458 comm30 : {a b : Obj Sets} ( x : One * FObj F b ) → ( Sets [ | |
| 459 FMap F (Iso.≅→ (mλ-iso isM)) o Sets [ φ o | |
| 460 FMap (m-bi MonoidalSets) ((λ _ → unit ) , id1 Sets (FObj F b) ) ] ] ) x ≡ Iso.≅→ (mλ-iso isM) x | |
| 461 comm30 {a} {b} ( OneObj , x) = begin | |
| 462 (FMap F (Iso.≅→ (mλ-iso isM))) ( φ ( unit , x ) ) | |
| 713 | 463 ≡⟨ IsHaskellMonoidalFunctor.law4 ismf ⟩ |
| 712 | 464 x |
| 465 ≡⟨⟩ | |
| 466 Iso.≅→ (mλ-iso isM) ( OneObj , x ) | |
| 467 ∎ | |
| 711 | 468 where |
| 713 | 469 open Relation.Binary.PropositionalEquality.≡-Reasoning |
| 709 | 470 comm3 : {a b : Obj Sets} → Sets [ Sets [ FMap F (Iso.≅→ (mλ-iso isM)) o |
| 711 | 471 Sets [ φ o FMap (m-bi MonoidalSets) ((λ _ → unit ) , id1 Sets (FObj F b)) ] ] ≈ Iso.≅→ (mλ-iso isM) ] |
| 712 | 472 comm3 {a} {b} = extensionality Sets ( λ x → comm30 {a} {b} x ) |
| 709 | 473 |
|
705
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
474 |
| 713 | 475 |
| 476 record IsApplicative {c₁ : Level} ( f : Functor (Sets {c₁}) (Sets {c₁}) ) | |
| 477 ( pure : {a : Obj Sets} → Hom Sets a ( FObj f a ) ) | |
| 478 ( _<*>_ : {a b : Obj Sets} → FObj f ( a → b ) → FObj f a → FObj f b ) | |
| 479 : Set (suc (suc c₁)) where | |
| 480 _・_ : { a b c : Obj (Sets {c₁} ) } → (b → c) → (a → b) → a → c | |
| 481 _・_ f g = λ x → f ( g x ) | |
| 482 field | |
| 483 identity : { a : Obj Sets } { u : FObj f a } → pure ( id1 Sets a ) <*> u ≡ u | |
| 484 composition : { a b c : Obj Sets } { u : FObj f ( b → c ) } { v : FObj f (a → b ) } { w : FObj f a } | |
| 485 → (( pure _・_ <*> u ) <*> v ) <*> w ≡ u <*> (v <*> w) | |
| 486 homomorphism : { a b : Obj Sets } { f : Hom Sets a b } { x : a } → pure f <*> pure x ≡ pure (f x) | |
| 487 interchange : { a b : Obj Sets } { u : FObj f ( a → b ) } { x : a } → u <*> pure x ≡ pure (λ f → f x) <*> u | |
| 488 | |
| 489 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
|
490 : Set (suc (suc c₁)) where |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
491 field |
| 713 | 492 pure : {a : Obj Sets} → Hom Sets a ( FObj F a ) |
| 493 <*> : {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
|
494 -- should have Applicative law |
|
705
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
495 |
| 713 | 496 lemma1 : {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) ) → Applicative F → HaskellMonoidalFunctor F |
| 497 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
|
498 where |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
499 open Applicative |
| 713 | 500 unit : FObj F One |
| 706 | 501 unit = pure app OneObj |
| 713 | 502 φ : {a b : Obj Sets} → Hom Sets ((FObj F a) * (FObj F b )) ( FObj F ( a * b ) ) |
| 503 φ {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
|
504 |
| 713 | 505 lemma2 : {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) ) → HaskellMonoidalFunctor F → Applicative F |
| 506 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
|
507 where |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
508 open HaskellMonoidalFunctor |
| 713 | 509 pure : {a : Obj Sets} → Hom Sets a ( FObj F a ) |
| 510 pure {a} x = FMap F ( λ y → x ) (unit mono) | |
| 511 <*> : {a b : Obj Sets} → FObj F ( a → b ) → FObj F a → FObj F b -- ** mono x y | |
| 512 <*> {a} {b} x y = FMap F ( λ a→b*b → ( proj₁ a→b*b ) ( proj₂ a→b*b ) ) (φ mono ( x , y )) | |
| 513 | |
| 514 open Relation.Binary.PropositionalEquality | |
| 515 | |
| 516 HaskellMonoidal→Applicative : {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) ) | |
| 517 ( unit : FObj F One ) | |
| 518 ( φ : {a b : Obj Sets} → Hom Sets ((FObj F a) * (FObj F b )) ( FObj F ( a * b ) ) ) | |
| 519 ( mono : IsHaskellMonoidalFunctor F unit φ ) | |
| 520 → IsApplicative F (λ x → FMap F ( λ y → x ) unit) (λ x y → FMap F ( λ a→b*b → ( proj₁ a→b*b ) ( proj₂ a→b*b ) ) (φ ( x , y ))) | |
| 521 HaskellMonoidal→Applicative {c₁} F unit φ mono = record { | |
| 522 identity = identity | |
| 523 ; composition = composition | |
| 524 ; homomorphism = homomorphism | |
| 525 ; interchange = interchange | |
| 526 } | |
| 527 where | |
| 528 isM : IsMonoidal (Sets {c₁}) One SetsTensorProduct | |
| 529 isM = Monoidal.isMonoidal MonoidalSets | |
| 530 open IsMonoidal | |
| 531 pure : {a : Obj Sets} → Hom Sets a ( FObj F a ) | |
| 532 pure {a} x = FMap F ( λ y → x ) (unit ) | |
| 533 _<*>_ : {a b : Obj Sets} → FObj F ( a → b ) → FObj F a → FObj F b | |
| 534 _<*>_ {a} {b} x y = FMap F ( λ a→b*b → ( proj₁ a→b*b ) ( proj₂ a→b*b ) ) (φ ( x , y )) | |
| 535 _・_ : { a b c : Obj (Sets {c₁} ) } → (b → c) → (a → b) → a → c | |
| 536 _・_ f g = λ x → f ( g x ) | |
| 537 identity : { a : Obj Sets } { u : FObj F a } → pure ( id1 Sets a ) <*> u ≡ u | |
| 538 identity {a} {u} = begin | |
| 539 pure ( id1 Sets a ) <*> u | |
| 540 ≡⟨⟩ | |
| 541 ( FMap F ( λ a→b*b → ( proj₁ a→b*b ) ( proj₂ a→b*b )) ) ( φ ( FMap F ( λ y → id1 Sets a ) unit , u ) ) | |
| 542 ≡⟨ sym ( ≡-cong ( λ k → ( FMap F ( λ a→b*b → ( proj₁ a→b*b ) ( proj₂ a→b*b )) ) ( φ ( FMap F ( λ y → id1 Sets a ) unit , k u ))) | |
| 543 ( IsFunctor.identity ( Functor.isFunctor F ) ) ) ⟩ | |
| 544 ( FMap F ( λ a→b*b → ( proj₁ a→b*b ) ( proj₂ a→b*b )) ) ( φ ( FMap F ( λ y → id1 Sets a ) unit , FMap F (id1 Sets a) u ) ) | |
| 545 ≡⟨ sym ( ≡-cong ( λ k → ( FMap F ( λ a→b*b → ( proj₁ a→b*b ) ( proj₂ a→b*b )) ) k ) ( IsHaskellMonoidalFunctor.law1 mono ) ) ⟩ | |
| 546 FMap F (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (FMap F (map (λ y → id1 Sets a) (λ x → x )) (φ (unit , u ))) | |
| 547 ≡⟨ ≡-cong ( λ k → k (φ (unit , u ) )) ( sym ( IsFunctor.distr ( Functor.isFunctor F ) ) ) ⟩ | |
| 548 FMap F (λ x → (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) ((map (λ y → id1 Sets a) (λ x → x )) x )) (φ (unit , u ) ) | |
| 549 ≡⟨⟩ | |
| 550 FMap F (λ x → proj₂ x ) (φ (unit , u ) ) | |
| 551 ≡⟨⟩ | |
| 552 FMap F (Iso.≅→ (mλ-iso isM)) (φ (unit , u )) | |
| 553 ≡⟨ IsHaskellMonoidalFunctor.law4 mono ⟩ | |
| 554 u | |
| 555 ∎ | |
| 556 where | |
| 557 open Relation.Binary.PropositionalEquality.≡-Reasoning | |
| 558 composition : { a b c : Obj Sets } { u : FObj F ( b → c ) } { v : FObj F (a → b ) } { w : FObj F a } | |
| 559 → (( pure _・_ <*> u ) <*> v ) <*> w ≡ u <*> (v <*> w) | |
| 560 composition {a} {b} {c} {u} {v} {w} = begin | |
| 561 ? | |
| 562 ≡⟨ ? ⟩ | |
| 563 ? | |
| 564 ∎ | |
| 565 where | |
| 566 open Relation.Binary.PropositionalEquality.≡-Reasoning | |
| 567 homomorphism : { a b : Obj Sets } { f : Hom Sets a b } { x : a } → pure f <*> pure x ≡ pure (f x) | |
| 568 homomorphism = {!!} | |
| 569 interchange : { a b : Obj Sets } { u : FObj F ( a → b ) } { x : a } → u <*> pure x ≡ pure (λ f → f x) <*> u | |
| 570 interchange = {!!} |