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