Mercurial > hg > Members > kono > Proof > category
annotate monoidal.agda @ 920:c10ee19a1ea3
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 04 May 2020 14:34:42 +0900 |
| parents | 340708e8d54f |
| children |
| 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 |
|
731
117e5b392673
Generalize Free Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
730
diff
changeset
|
14 -- record Iso {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ) |
|
117e5b392673
Generalize Free Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
730
diff
changeset
|
15 -- (x y : Obj C ) |
|
117e5b392673
Generalize Free Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
730
diff
changeset
|
16 -- : Set ( suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where |
|
117e5b392673
Generalize Free Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
730
diff
changeset
|
17 -- field |
|
117e5b392673
Generalize Free Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
730
diff
changeset
|
18 -- ≅→ : Hom C x y |
|
117e5b392673
Generalize Free Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
730
diff
changeset
|
19 -- ≅← : Hom C y x |
|
117e5b392673
Generalize Free Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
730
diff
changeset
|
20 -- iso→ : C [ C [ ≅← o ≅→ ] ≈ id1 C x ] |
|
117e5b392673
Generalize Free Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
730
diff
changeset
|
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 |
| 730 | 23 -- Monoidal Category |
| 698 | 24 |
| 25 record IsMonoidal {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ) (I : Obj C) ( BI : Functor ( C × C ) C ) | |
| 26 : Set ( suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where | |
| 27 open Iso | |
|
700
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
28 infixr 9 _□_ _■_ |
|
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
29 _□_ : ( x y : Obj C ) → Obj C |
|
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
30 _□_ x y = FObj BI ( x , y ) |
|
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
31 _■_ : {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
|
32 _■_ f g = FMap BI ( f , g ) |
| 698 | 33 field |
|
700
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
34 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
|
35 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
|
36 mρ-iso : {a : Obj C} → Iso C ( a □ I) a |
| 698 | 37 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
|
38 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
|
39 C [ ≅→ (mα-iso ) o ( (f ■ id1 C b ) ■ id1 C c ) ] ] |
| 698 | 40 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
|
41 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
|
42 C [ ≅→ (mα-iso ) o ( (id1 C a ■ f ) ■ id1 C c ) ] ] |
| 698 | 43 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
|
44 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
|
45 C [ ≅→ (mα-iso ) o ( id1 C ( a □ b ) ■ f ) ] ] |
| 698 | 46 mλ→nat : {a a' : Obj C} → ( f : Hom C a a' ) → |
| 47 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
|
48 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
|
49 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
|
50 C [ C [ f o ≅→ (mρ-iso {a} ) ] ≈ |
|
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
51 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
|
52 -- 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
|
53 α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
|
54 α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
|
55 α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
|
56 α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
|
57 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
|
58 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
|
59 α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
|
60 α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
|
61 α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
|
62 α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
|
63 α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
|
64 αAIB {a} {b} = ≅→ mα-iso |
|
700
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
65 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
|
66 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
|
67 ρ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
|
68 ρ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
|
69 |
|
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
70 field |
|
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
71 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
|
72 → 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
|
73 ≈ αA□BCD {a} {b} {c} {d} {e} ] |
|
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
74 comm-unit : {a b : Obj C} |
|
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
75 → 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
|
76 |
|
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
77 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
|
78 : Set ( suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where |
|
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
79 field |
|
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
80 m-i : Obj C |
|
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
81 m-bi : Functor ( C × C ) C |
|
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
82 isMonoidal : IsMonoidal C m-i m-bi |
|
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
83 |
|
705
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
84 --------- |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
85 -- |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
86 -- Lax Monoidal Functor |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
87 -- |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
88 -- N → M |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
89 -- |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
90 --------- |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
91 |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
92 --------- |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
93 -- |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
94 -- 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
|
95 -- 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
|
96 -- |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
97 -- F x ● F y |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
98 -- F ( x ⊗ y ) |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
99 -- |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
100 -- 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
|
101 -- |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
102 -- φ : 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
|
103 -- |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
104 -- 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
|
105 -- |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
106 -- a given unit arrow |
|
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 -- ψ : IN → IM |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
109 |
| 703 | 110 Functor● : {c₁ c₂ ℓ : Level} (C D : Category c₁ c₂ ℓ) ( N : Monoidal D ) |
| 111 ( MF : Functor C D ) → Functor ( C × C ) D | |
| 112 Functor● C D N MF = record { | |
| 113 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
|
114 ; FMap = λ {x : Obj ( C × C ) } {y} f → ( FMap MF (proj₁ f ) ■ FMap MF (proj₂ f) ) |
| 703 | 115 ; isFunctor = record { |
| 116 ≈-cong = ≈-cong | |
| 117 ; identity = identity | |
| 118 ; distr = distr | |
| 119 } | |
| 120 } where | |
| 121 _●_ : (x y : Obj D ) → Obj D | |
| 122 _●_ x y = (IsMonoidal._□_ (Monoidal.isMonoidal N) ) x y | |
| 704 | 123 _■_ : {a b c d : Obj D } ( f : Hom D a c ) ( g : Hom D b d ) → Hom D ( a ● b ) ( c ● d ) |
| 124 _■_ f g = FMap (Monoidal.m-bi N) ( f , g ) | |
| 125 F : { a b : Obj C } → ( f : Hom C a b ) → Hom D (FObj MF a) (FObj MF b ) | |
| 126 F f = FMap MF f | |
| 703 | 127 ≈-cong : {a b : Obj (C × C)} {f g : Hom (C × C) a b} → (C × C) [ f ≈ g ] → |
| 704 | 128 D [ (F (proj₁ f) ■ F (proj₂ f)) ≈ (F (proj₁ g) ■ F (proj₂ g)) ] |
| 703 | 129 ≈-cong {a} {b} {f} {g} f≈g = let open ≈-Reasoning D in begin |
| 704 | 130 F (proj₁ f) ■ F (proj₂ f) |
| 703 | 131 ≈⟨ fcong (Monoidal.m-bi N) ( fcong MF ( proj₁ f≈g ) , fcong MF ( proj₂ f≈g )) ⟩ |
| 704 | 132 F (proj₁ g) ■ F (proj₂ g) |
| 703 | 133 ∎ |
| 704 | 134 identity : {a : Obj (C × C)} → D [ (F (proj₁ (id1 (C × C) a)) ■ F (proj₂ (id1 (C × C) a))) |
| 703 | 135 ≈ id1 D (FObj MF (proj₁ a) ● FObj MF (proj₂ a)) ] |
| 136 identity {a} = let open ≈-Reasoning D in begin | |
| 704 | 137 F (proj₁ (id1 (C × C) a)) ■ F (proj₂ (id1 (C × C) a)) |
| 703 | 138 ≈⟨ fcong (Monoidal.m-bi N) ( IsFunctor.identity (isFunctor MF ) , IsFunctor.identity (isFunctor MF )) ⟩ |
| 704 | 139 id1 D (FObj MF (proj₁ a)) ■ id1 D (FObj MF (proj₂ a)) |
| 703 | 140 ≈⟨ IsFunctor.identity (isFunctor (Monoidal.m-bi N)) ⟩ |
| 141 id1 D (FObj MF (proj₁ a) ● FObj MF (proj₂ a)) | |
| 142 ∎ | |
| 143 distr : {a b c : Obj (C × C)} {f : Hom (C × C) a b} {g : Hom (C × C) b c} → | |
| 704 | 144 D [ (F (proj₁ ((C × C) [ g o f ])) ■ F (proj₂ ((C × C) [ g o f ]))) |
| 145 ≈ D [ (F (proj₁ g) ■ F (proj₂ g)) o (F (proj₁ f) ■ F (proj₂ f)) ] ] | |
| 703 | 146 distr {a} {b} {c} {f} {g} = let open ≈-Reasoning D in begin |
| 704 | 147 (F (proj₁ ((C × C) [ g o f ])) ■ F (proj₂ ((C × C) [ g o f ]))) |
| 703 | 148 ≈⟨ fcong (Monoidal.m-bi N) ( IsFunctor.distr ( isFunctor MF) , IsFunctor.distr ( isFunctor MF )) ⟩ |
| 704 | 149 ( F (proj₁ g) o F (proj₁ f) ) ■ ( F (proj₂ g) o F (proj₂ f) ) |
| 703 | 150 ≈⟨ IsFunctor.distr ( isFunctor (Monoidal.m-bi N)) ⟩ |
| 704 | 151 (F (proj₁ g) ■ F (proj₂ g)) o (F (proj₁ f) ■ F (proj₂ f)) |
| 703 | 152 ∎ |
|
696
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
153 |
| 703 | 154 Functor⊗ : {c₁ c₂ ℓ : Level} (C D : Category c₁ c₂ ℓ) ( M : Monoidal C ) |
| 155 ( MF : Functor C D ) → Functor ( C × C ) D | |
| 156 Functor⊗ C D M MF = record { | |
| 157 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
|
158 ; FMap = λ {a} {b} f → F ( proj₁ f □ proj₂ f ) |
| 703 | 159 ; isFunctor = record { |
| 160 ≈-cong = ≈-cong | |
| 161 ; identity = identity | |
| 162 ; distr = distr | |
| 163 } | |
| 164 } where | |
| 165 _⊗_ : (x y : Obj C ) → Obj C | |
| 166 _⊗_ x y = (IsMonoidal._□_ (Monoidal.isMonoidal M) ) x y | |
| 704 | 167 _□_ : {a b c d : Obj C } ( f : Hom C a c ) ( g : Hom C b d ) → Hom C ( a ⊗ b ) ( c ⊗ d ) |
| 168 _□_ f g = FMap (Monoidal.m-bi M) ( f , g ) | |
| 169 F : { a b : Obj C } → ( f : Hom C a b ) → Hom D (FObj MF a) (FObj MF b ) | |
| 170 F f = FMap MF f | |
| 703 | 171 ≈-cong : {a b : Obj (C × C)} {f g : Hom (C × C) a b} → (C × C) [ f ≈ g ] → |
| 704 | 172 D [ F ( (proj₁ f □ proj₂ f)) ≈ F ( (proj₁ g □ proj₂ g)) ] |
| 703 | 173 ≈-cong {a} {b} {f} {g} f≈g = IsFunctor.≈-cong (isFunctor MF ) ( IsFunctor.≈-cong (isFunctor (Monoidal.m-bi M) ) f≈g ) |
| 704 | 174 identity : {a : Obj (C × C)} → D [ F ( (proj₁ (id1 (C × C) a) □ proj₂ (id1 (C × C) a))) |
| 703 | 175 ≈ id1 D (FObj MF (proj₁ a ⊗ proj₂ a)) ] |
| 176 identity {a} = let open ≈-Reasoning D in begin | |
| 704 | 177 F ( (proj₁ (id1 (C × C) a) □ proj₂ (id1 (C × C) a))) |
| 703 | 178 ≈⟨⟩ |
| 704 | 179 F (FMap (Monoidal.m-bi M) (id1 (C × C) a ) ) |
| 703 | 180 ≈⟨ fcong MF ( IsFunctor.identity (isFunctor (Monoidal.m-bi M) )) ⟩ |
| 704 | 181 F (id1 C (proj₁ a ⊗ proj₂ a)) |
| 703 | 182 ≈⟨ IsFunctor.identity (isFunctor MF) ⟩ |
| 183 id1 D (FObj MF (proj₁ a ⊗ proj₂ a)) | |
| 184 ∎ | |
| 185 distr : {a b c : Obj (C × C)} {f : Hom (C × C) a b} {g : Hom (C × C) b c} → D [ | |
| 704 | 186 F ( (proj₁ ((C × C) [ g o f ]) □ proj₂ ((C × C) [ g o f ]))) |
| 187 ≈ D [ F ( (proj₁ g □ proj₂ g)) o F ( (proj₁ f □ proj₂ f)) ] ] | |
| 703 | 188 distr {a} {b} {c} {f} {g} = let open ≈-Reasoning D in begin |
| 704 | 189 F ( (proj₁ ((C × C) [ g o f ]) □ proj₂ ((C × C) [ g o f ]))) |
| 703 | 190 ≈⟨⟩ |
| 704 | 191 F (FMap (Monoidal.m-bi M) ( (C × C) [ g o f ] )) |
| 703 | 192 ≈⟨ fcong MF ( IsFunctor.distr (isFunctor (Monoidal.m-bi M))) ⟩ |
| 704 | 193 F (C [ FMap (Monoidal.m-bi M) g o FMap (Monoidal.m-bi M) f ]) |
| 703 | 194 ≈⟨ IsFunctor.distr ( isFunctor MF ) ⟩ |
| 704 | 195 F ( proj₁ g □ proj₂ g) o F ( proj₁ f □ proj₂ f) |
| 703 | 196 ∎ |
| 197 | |
|
696
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
198 |
|
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
199 record IsMonoidalFunctor {c₁ c₂ ℓ : Level} {C D : Category c₁ c₂ ℓ} ( M : Monoidal C ) ( N : Monoidal D ) |
| 698 | 200 ( MF : Functor C D ) |
|
702
d16327b48b83
Monoidal Functor ( two functor remains )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
701
diff
changeset
|
201 ( ψ : 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
|
202 : Set ( suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where |
| 698 | 203 _⊗_ : (x y : Obj C ) → Obj C |
|
700
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
204 _⊗_ 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
|
205 _□_ : {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
|
206 _□_ f g = FMap (Monoidal.m-bi M) ( f , g ) |
| 698 | 207 _●_ : (x y : Obj D ) → Obj D |
|
700
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
208 _●_ 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
|
209 _■_ : {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
|
210 _■_ 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
|
211 F● : Functor ( C × C ) D |
| 703 | 212 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
|
213 F⊗ : Functor ( C × C ) D |
| 703 | 214 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
|
215 field |
|
d16327b48b83
Monoidal Functor ( two functor remains )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
701
diff
changeset
|
216 φab : NTrans ( C × C ) D F● F⊗ |
| 698 | 217 open Iso |
| 218 open Monoidal | |
|
701
7a729bb62ce3
Monoidal Functor on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
700
diff
changeset
|
219 open IsMonoidal hiding ( _■_ ; _□_ ) |
| 699 | 220 αC : {a b c : Obj C} → Hom C (( a ⊗ b ) ⊗ c ) ( a ⊗ ( b ⊗ c ) ) |
| 221 αC {a} {b} {c} = ≅→ (mα-iso (isMonoidal M) {a} {b} {c}) | |
| 222 αD : {a b c : Obj D} → Hom D (( a ● b ) ● c ) ( a ● ( b ● c ) ) | |
| 223 α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
|
224 F : Obj C → Obj D |
|
7a729bb62ce3
Monoidal Functor on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
700
diff
changeset
|
225 F x = FObj MF x |
|
702
d16327b48b83
Monoidal Functor ( two functor remains )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
701
diff
changeset
|
226 φ : ( 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
|
227 φ 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
|
228 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
|
229 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
|
230 φ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
|
231 φ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
|
232 φ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
|
233 φ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
|
234 φ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
|
235 φ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
|
236 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
|
237 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
|
238 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
|
239 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
|
240 φ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
|
241 φ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
|
242 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
|
243 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
|
244 ρ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
|
245 ρ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
|
246 ψ●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
|
247 ψ●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
|
248 φ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
|
249 φ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
|
250 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
|
251 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
|
252 λ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
|
253 λ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
|
254 field |
|
705
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
255 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
|
256 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
|
257 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
|
258 |
|
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
259 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
|
260 : 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
|
261 field |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
262 MF : Functor C D |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
263 ψ : 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
|
264 isMonodailFunctor : IsMonoidalFunctor M N MF ψ |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
265 |
|
731
117e5b392673
Generalize Free Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
730
diff
changeset
|
266 |
|
705
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
267 open import Category.Sets |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
268 |
| 706 | 269 import Relation.Binary.PropositionalEquality |
| 270 -- 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 ) | |
| 271 postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂ | |
| 272 | |
| 730 | 273 ------ |
| 274 -- Data.Product as a Tensor Product for Monoidal Category | |
| 275 -- | |
|
705
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
276 |
| 781 | 277 open import Relation.Binary.PropositionalEquality hiding ( [_] ) |
| 278 | |
| 708 | 279 SetsTensorProduct : {c : Level} → Functor ( Sets {c} × Sets {c} ) (Sets {c}) |
| 280 SetsTensorProduct = record { | |
| 281 FObj = λ x → proj₁ x * proj₂ x | |
| 282 ; FMap = λ {x : Obj ( Sets × Sets ) } {y} f → map (proj₁ f) (proj₂ f) | |
| 283 ; isFunctor = record { | |
| 284 ≈-cong = ≈-cong | |
| 285 ; identity = refl | |
| 286 ; distr = refl | |
| 706 | 287 } |
| 708 | 288 } where |
| 289 ≈-cong : {a b : Obj (Sets × Sets)} {f g : Hom (Sets × Sets) a b} → | |
| 290 (Sets × Sets) [ f ≈ g ] → Sets [ map (proj₁ f) (proj₂ f) ≈ map (proj₁ g) (proj₂ g) ] | |
| 291 ≈-cong (refl , refl) = refl | |
| 292 | |
| 730 | 293 ----- |
| 294 -- | |
| 295 -- Sets as Monoidal Category | |
| 296 -- | |
| 297 -- almost all comutativities are refl | |
| 298 -- | |
| 299 -- | |
| 300 -- | |
| 708 | 301 |
| 730 | 302 data One {c : Level} : Set c where |
| 303 OneObj : One -- () in Haskell ( or any one object set ) | |
| 708 | 304 |
| 305 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
|
306 MonoidalSets {c} = record { |
|
ea84cc6c1797
monoidal functor and applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
726
diff
changeset
|
307 m-i = One {c} ; |
| 708 | 308 m-bi = SetsTensorProduct ; |
| 309 isMonoidal = record { | |
| 310 mα-iso = record { ≅→ = mα→ ; ≅← = mα← ; iso→ = refl ; iso← = refl } ; | |
| 311 mλ-iso = record { ≅→ = mλ→ ; ≅← = mλ← ; iso→ = extensionality Sets ( λ x → mλiso x ) ; iso← = refl } ; | |
| 312 mρ-iso = record { ≅→ = mρ→ ; ≅← = mρ← ; iso→ = extensionality Sets ( λ x → mρiso x ) ; iso← = refl } ; | |
| 313 mα→nat1 = λ f → refl ; | |
| 314 mα→nat2 = λ f → refl ; | |
| 315 mα→nat3 = λ f → refl ; | |
| 316 mλ→nat = λ f → refl ; | |
| 317 mρ→nat = λ f → refl ; | |
| 318 comm-penta = refl ; | |
| 319 comm-unit = refl | |
| 320 } | |
| 321 } where | |
| 322 _⊗_ : ( a b : Obj Sets ) → Obj Sets | |
| 323 _⊗_ a b = FObj SetsTensorProduct (a , b ) | |
| 770 | 324 -- associative operations |
| 708 | 325 mα→ : {a b c : Obj Sets} → Hom Sets ( ( a ⊗ b ) ⊗ c ) ( a ⊗ ( b ⊗ c ) ) |
| 326 mα→ ((a , b) , c ) = (a , ( b , c ) ) | |
| 327 mα← : {a b c : Obj Sets} → Hom Sets ( a ⊗ ( b ⊗ c ) ) ( ( a ⊗ b ) ⊗ c ) | |
| 328 mα← (a , ( b , c ) ) = ((a , b) , c ) | |
| 730 | 329 -- (One , a) ⇔ a |
| 708 | 330 mλ→ : {a : Obj Sets} → Hom Sets ( One ⊗ a ) a |
| 331 mλ→ (_ , a) = a | |
| 332 mλ← : {a : Obj Sets} → Hom Sets a ( One ⊗ a ) | |
| 333 mλ← a = ( OneObj , a ) | |
| 334 mλiso : {a : Obj Sets} (x : One ⊗ a) → (Sets [ mλ← o mλ→ ]) x ≡ id1 Sets (One ⊗ a) x | |
| 335 mλiso (OneObj , _ ) = refl | |
| 730 | 336 -- (a , One) ⇔ a |
| 708 | 337 mρ→ : {a : Obj Sets} → Hom Sets ( a ⊗ One ) a |
| 338 mρ→ (a , _) = a | |
| 339 mρ← : {a : Obj Sets} → Hom Sets a ( a ⊗ One ) | |
| 340 mρ← a = ( a , OneObj ) | |
| 341 mρiso : {a : Obj Sets} (x : a ⊗ One ) → (Sets [ mρ← o mρ→ ]) x ≡ id1 Sets (a ⊗ One) x | |
| 342 mρiso (_ , OneObj ) = refl | |
| 343 | |
| 710 | 344 ≡-cong = Relation.Binary.PropositionalEquality.cong |
| 706 | 345 |
| 769 | 346 ---- |
| 347 -- | |
| 348 -- HaskellMonoidalFunctor is a monoidal functor on Sets | |
| 349 -- | |
| 350 -- | |
| 351 | |
| 713 | 352 |
| 353 record IsHaskellMonoidalFunctor {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) ) | |
| 354 ( unit : FObj F One ) | |
| 355 ( φ : {a b : Obj Sets} → Hom Sets ((FObj F a) * (FObj F b )) ( FObj F ( a * b ) ) ) | |
| 356 : Set (suc (suc c₁)) where | |
| 357 isM : IsMonoidal (Sets {c₁}) One SetsTensorProduct | |
| 358 isM = Monoidal.isMonoidal MonoidalSets | |
| 359 open IsMonoidal | |
| 360 field | |
| 715 | 361 natφ : { a b c d : Obj Sets } { x : FObj F a} { y : FObj F b} { f : a → c } { g : b → d } |
| 713 | 362 → FMap F (map f g) (φ (x , y)) ≡ φ (FMap F f x , FMap F g y) |
| 715 | 363 assocφ : { x y z : Obj Sets } { a : FObj F x } { b : FObj F y }{ c : FObj F z } |
| 713 | 364 → φ (a , φ (b , c)) ≡ FMap F (Iso.≅→ (mα-iso isM)) (φ (φ (a , b) , c)) |
| 715 | 365 idrφ : {a : Obj Sets } { x : FObj F a } → FMap F (Iso.≅→ (mρ-iso isM)) (φ (x , unit)) ≡ x |
| 366 idlφ : {a : Obj Sets } { x : FObj F a } → FMap F (Iso.≅→ (mλ-iso isM)) (φ (unit , x)) ≡ x | |
| 713 | 367 |
| 714 | 368 -- http://www.staff.city.ac.uk/~ross/papers/Applicative.pdf |
| 369 -- naturality of φ fmap(f × g)(φ u v) = φ ( fmap f u) ( fmap g v ) | |
| 370 -- left identity fmap snd (φ unit v) = v | |
| 371 -- right identity fmap fst (φ u unit) = u | |
| 372 -- associativity fmap assoc (φ u (φ v w)) = φ (φ u v) w | |
| 373 | |
| 374 | |
| 730 | 375 record HaskellMonoidalFunctor {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
|
376 : Set (suc (suc c₁)) where |
|
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
377 field |
| 730 | 378 unit : FObj F One |
| 379 φ : {a b : Obj Sets} → Hom Sets ((FObj F a) * (FObj F b )) ( FObj F ( a * b ) ) | |
| 766 | 380 isHaskellMonoidalFunctor : IsHaskellMonoidalFunctor F unit φ |
|
705
73a998711118
add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
704
diff
changeset
|
381 |
| 769 | 382 |
| 383 ---- | |
| 384 -- | |
| 385 -- laws of HaskellMonoidalFunctor are directly mapped to the laws of Monoidal Functor | |
| 386 -- | |
| 387 -- | |
| 388 | |
| 730 | 389 HaskellMonoidalFunctor→MonoidalFunctor : {c : Level} ( F : Functor (Sets {c}) (Sets {c}) ) → (mf : HaskellMonoidalFunctor F ) |
| 713 | 390 → MonoidalFunctor {_} {c} {_} {Sets} {Sets} MonoidalSets MonoidalSets |
| 766 | 391 HaskellMonoidalFunctor→MonoidalFunctor {c} F mf = 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 ( _■_ ; _□_ ) | |
| 766 | 403 ismf : IsHaskellMonoidalFunctor F ( HaskellMonoidalFunctor.unit mf ) ( HaskellMonoidalFunctor.φ mf ) |
| 404 ismf = HaskellMonoidalFunctor.isHaskellMonoidalFunctor mf | |
| 730 | 405 M : Monoidal (Sets {c}) |
| 709 | 406 M = MonoidalSets |
| 730 | 407 isM : IsMonoidal (Sets {c}) One SetsTensorProduct |
| 709 | 408 isM = Monoidal.isMonoidal MonoidalSets |
| 730 | 409 unit : FObj F One |
| 709 | 410 unit = HaskellMonoidalFunctor.unit mf |
| 411 _⊗_ : (x y : Obj Sets ) → Obj Sets | |
| 412 _⊗_ x y = (IsMonoidal._□_ (Monoidal.isMonoidal M) ) x y | |
| 413 _□_ : {a b c d : Obj Sets } ( f : Hom Sets a c ) ( g : Hom Sets b d ) → Hom Sets ( a ⊗ b ) ( c ⊗ d ) | |
| 414 _□_ f g = FMap (m-bi M) ( f , g ) | |
| 711 | 415 φ : {x : Obj (Sets × Sets) } → Hom Sets (FObj (Functor● Sets Sets MonoidalSets F) x) (FObj (Functor⊗ Sets Sets MonoidalSets F) x) |
| 416 φ z = HaskellMonoidalFunctor.φ mf z | |
| 710 | 417 comm00 : {a b : Obj (Sets × Sets)} { f : Hom (Sets × Sets) a b} (x : ( FObj F (proj₁ a) * FObj F (proj₂ a)) ) → |
| 711 | 418 (Sets [ FMap (Functor⊗ Sets Sets MonoidalSets F) f o φ ]) x ≡ (Sets [ φ o FMap (Functor● Sets Sets MonoidalSets F) f ]) x |
| 710 | 419 comm00 {a} {b} {(f , g)} (x , y) = begin |
| 711 | 420 (FMap (Functor⊗ Sets Sets MonoidalSets F) (f , g) ) (φ (x , y)) |
| 710 | 421 ≡⟨⟩ |
| 711 | 422 (FMap F ( f □ g ) ) (φ (x , y)) |
| 710 | 423 ≡⟨⟩ |
| 711 | 424 FMap F ( map f g ) (φ (x , y)) |
| 715 | 425 ≡⟨ IsHaskellMonoidalFunctor.natφ ismf ⟩ |
| 711 | 426 φ ( FMap F f x , FMap F g y ) |
| 710 | 427 ≡⟨⟩ |
| 711 | 428 φ ( ( FMap F f □ FMap F g ) (x , y) ) |
| 710 | 429 ≡⟨⟩ |
| 711 | 430 φ ((FMap (Functor● Sets Sets MonoidalSets F) (f , g) ) (x , y) ) |
| 710 | 431 ∎ |
| 432 where | |
| 713 | 433 open Relation.Binary.PropositionalEquality.≡-Reasoning |
| 711 | 434 comm0 : {a b : Obj (Sets × Sets)} { f : Hom (Sets × Sets) a b} → Sets [ Sets [ FMap (Functor⊗ Sets Sets MonoidalSets F) f o φ ] |
| 435 ≈ Sets [ φ o FMap (Functor● Sets Sets MonoidalSets F) f ] ] | |
| 710 | 436 comm0 {a} {b} {f} = extensionality Sets ( λ (x : ( FObj F (proj₁ a) * FObj F (proj₂ a)) ) → comm00 x ) |
| 711 | 437 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 ≡ |
| 438 (Sets [ FMap F (Iso.≅→ (mα-iso isM)) o Sets [ φ o φ □ id1 Sets (FObj F c) ] ]) x | |
| 710 | 439 comm10 {x} {y} {f} ((a , b) , c ) = begin |
| 711 | 440 φ (( id1 Sets (FObj F x) □ φ ) ( ( Iso.≅→ (mα-iso isM) ) ((a , b) , c))) |
| 710 | 441 ≡⟨⟩ |
| 711 | 442 φ ( a , φ (b , c)) |
| 715 | 443 ≡⟨ IsHaskellMonoidalFunctor.assocφ ismf ⟩ |
| 711 | 444 ( FMap F (Iso.≅→ (mα-iso isM))) (φ (( φ (a , b)) , c )) |
| 710 | 445 ≡⟨⟩ |
| 711 | 446 ( FMap F (Iso.≅→ (mα-iso isM))) (φ (( φ □ id1 Sets (FObj F f) ) ((a , b) , c))) |
| 710 | 447 ∎ |
| 448 where | |
| 713 | 449 open Relation.Binary.PropositionalEquality.≡-Reasoning |
| 711 | 450 comm1 : {a b c : Obj Sets} → Sets [ Sets [ φ |
| 451 o Sets [ (id1 Sets (FObj F a) □ φ ) o Iso.≅→ (mα-iso isM) ] ] | |
| 452 ≈ Sets [ FMap F (Iso.≅→ (mα-iso isM)) o Sets [ φ o (φ □ id1 Sets (FObj F c)) ] ] ] | |
| 710 | 453 comm1 {a} {b} {c} = extensionality Sets ( λ x → comm10 x ) |
| 712 | 454 comm20 : {a b : Obj Sets} ( x : FObj F a * One ) → ( Sets [ |
| 455 FMap F (Iso.≅→ (mρ-iso isM)) o Sets [ φ o | |
| 456 FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit )) ] ] ) x ≡ Iso.≅→ (mρ-iso isM) x | |
| 457 comm20 {a} {b} (x , OneObj ) = begin | |
| 458 (FMap F (Iso.≅→ (mρ-iso isM))) ( φ ( x , unit ) ) | |
| 715 | 459 ≡⟨ IsHaskellMonoidalFunctor.idrφ ismf ⟩ |
| 712 | 460 x |
| 461 ≡⟨⟩ | |
| 462 Iso.≅→ (mρ-iso isM) ( x , OneObj ) | |
| 463 ∎ | |
| 464 where | |
| 713 | 465 open Relation.Binary.PropositionalEquality.≡-Reasoning |
| 709 | 466 comm2 : {a b : Obj Sets} → Sets [ Sets [ |
| 711 | 467 FMap F (Iso.≅→ (mρ-iso isM)) o Sets [ φ o |
| 709 | 468 FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit )) ] ] ≈ Iso.≅→ (mρ-iso isM) ] |
| 712 | 469 comm2 {a} {b} = extensionality Sets ( λ x → comm20 {a} {b} x ) |
| 470 comm30 : {a b : Obj Sets} ( x : One * FObj F b ) → ( Sets [ | |
| 471 FMap F (Iso.≅→ (mλ-iso isM)) o Sets [ φ o | |
| 472 FMap (m-bi MonoidalSets) ((λ _ → unit ) , id1 Sets (FObj F b) ) ] ] ) x ≡ Iso.≅→ (mλ-iso isM) x | |
| 473 comm30 {a} {b} ( OneObj , x) = begin | |
| 474 (FMap F (Iso.≅→ (mλ-iso isM))) ( φ ( unit , x ) ) | |
| 715 | 475 ≡⟨ IsHaskellMonoidalFunctor.idlφ ismf ⟩ |
| 712 | 476 x |
| 477 ≡⟨⟩ | |
| 478 Iso.≅→ (mλ-iso isM) ( OneObj , x ) | |
| 479 ∎ | |
| 711 | 480 where |
| 713 | 481 open Relation.Binary.PropositionalEquality.≡-Reasoning |
| 709 | 482 comm3 : {a b : Obj Sets} → Sets [ Sets [ FMap F (Iso.≅→ (mλ-iso isM)) o |
| 711 | 483 Sets [ φ o FMap (m-bi MonoidalSets) ((λ _ → unit ) , id1 Sets (FObj F b)) ] ] ≈ Iso.≅→ (mλ-iso isM) ] |
| 712 | 484 comm3 {a} {b} = extensionality Sets ( λ x → comm30 {a} {b} x ) |
| 709 | 485 |
| 769 | 486 -- end |