Mercurial > hg > Members > kono > Proof > category

annotate monoidal.agda @ 768:9bcdbfbaaa39

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clean up
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 12 Dec 2017 10:25:59 +0900
parents c30ca91f3a76
children 43138aead09b
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
e4ef69bae044 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 729
diff changeset
23 -- Monoidal Category
698
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
24
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
25 record IsMonoidal {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ) (I : Obj C) ( BI : Functor ( C × C ) C )
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
26 : Set ( suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
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
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
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
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
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
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
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
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
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
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
46 mλ→nat : {a a' : Obj C} → ( f : Hom C a a' ) →
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
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
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
110 Functor● : {c₁ c₂ ℓ : Level} (C D : Category c₁ c₂ ℓ) ( N : Monoidal D )
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
111 ( MF : Functor C D ) → Functor ( C × C ) D
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
112 Functor● C D N MF = record {
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
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
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
115 ; isFunctor = record {
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
116 ≈-cong = ≈-cong
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
117 ; identity = identity
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
118 ; distr = distr
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
119 }
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
120 } where
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
121 _●_ : (x y : Obj D ) → Obj D
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
122 _●_ x y = (IsMonoidal._□_ (Monoidal.isMonoidal N) ) x y
704
b48c2d1c0796 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 703
diff changeset
123 _■_ : {a b c d : Obj D } ( f : Hom D a c ) ( g : Hom D b d ) → Hom D ( a ● b ) ( c ● d )
b48c2d1c0796 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 703
diff changeset
124 _■_ f g = FMap (Monoidal.m-bi N) ( f , g )
b48c2d1c0796 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 703
diff changeset
125 F : { a b : Obj C } → ( f : Hom C a b ) → Hom D (FObj MF a) (FObj MF b )
b48c2d1c0796 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 703
diff changeset
126 F f = FMap MF f
703
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
127 ≈-cong : {a b : Obj (C × C)} {f g : Hom (C × C) a b} → (C × C) [ f ≈ g ] →
704
b48c2d1c0796 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 703
diff changeset
128 D [ (F (proj₁ f) ■ F (proj₂ f)) ≈ (F (proj₁ g) ■ F (proj₂ g)) ]
703
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
129 ≈-cong {a} {b} {f} {g} f≈g = let open ≈-Reasoning D in begin
704
b48c2d1c0796 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 703
diff changeset
130 F (proj₁ f) ■ F (proj₂ f)
703
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
131 ≈⟨ fcong (Monoidal.m-bi N) ( fcong MF ( proj₁ f≈g ) , fcong MF ( proj₂ f≈g )) ⟩
704
b48c2d1c0796 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 703
diff changeset
132 F (proj₁ g) ■ F (proj₂ g)
703
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
133 ∎
704
b48c2d1c0796 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 703
diff changeset
134 identity : {a : Obj (C × C)} → D [ (F (proj₁ (id1 (C × C) a)) ■ F (proj₂ (id1 (C × C) a)))
703
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
135 ≈ id1 D (FObj MF (proj₁ a) ● FObj MF (proj₂ a)) ]
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
136 identity {a} = let open ≈-Reasoning D in begin
704
b48c2d1c0796 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 703
diff changeset
137 F (proj₁ (id1 (C × C) a)) ■ F (proj₂ (id1 (C × C) a))
703
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
138 ≈⟨ fcong (Monoidal.m-bi N) ( IsFunctor.identity (isFunctor MF ) , IsFunctor.identity (isFunctor MF )) ⟩
704
b48c2d1c0796 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 703
diff changeset
139 id1 D (FObj MF (proj₁ a)) ■ id1 D (FObj MF (proj₂ a))
703
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
140 ≈⟨ IsFunctor.identity (isFunctor (Monoidal.m-bi N)) ⟩
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
141 id1 D (FObj MF (proj₁ a) ● FObj MF (proj₂ a))
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
142 ∎
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
143 distr : {a b c : Obj (C × C)} {f : Hom (C × C) a b} {g : Hom (C × C) b c} →
704
b48c2d1c0796 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 703
diff changeset
144 D [ (F (proj₁ ((C × C) [ g o f ])) ■ F (proj₂ ((C × C) [ g o f ])))
b48c2d1c0796 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 703
diff changeset
145 ≈ D [ (F (proj₁ g) ■ F (proj₂ g)) o (F (proj₁ f) ■ F (proj₂ f)) ] ]
703
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
146 distr {a} {b} {c} {f} {g} = let open ≈-Reasoning D in begin
704
b48c2d1c0796 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 703
diff changeset
147 (F (proj₁ ((C × C) [ g o f ])) ■ F (proj₂ ((C × C) [ g o f ])))
703
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
148 ≈⟨ fcong (Monoidal.m-bi N) ( IsFunctor.distr ( isFunctor MF) , IsFunctor.distr ( isFunctor MF )) ⟩
704
b48c2d1c0796 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 703
diff changeset
149 ( F (proj₁ g) o F (proj₁ f) ) ■ ( F (proj₂ g) o F (proj₂ f) )
703
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
150 ≈⟨ IsFunctor.distr ( isFunctor (Monoidal.m-bi N)) ⟩
704
b48c2d1c0796 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 703
diff changeset
151 (F (proj₁ g) ■ F (proj₂ g)) o (F (proj₁ f) ■ F (proj₂ f))
703
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
152 ∎
696
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
153
703
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
154 Functor⊗ : {c₁ c₂ ℓ : Level} (C D : Category c₁ c₂ ℓ) ( M : Monoidal C )
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
155 ( MF : Functor C D ) → Functor ( C × C ) D
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
156 Functor⊗ C D M MF = record {
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
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
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
159 ; isFunctor = record {
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
160 ≈-cong = ≈-cong
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
161 ; identity = identity
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
162 ; distr = distr
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
163 }
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
164 } where
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
165 _⊗_ : (x y : Obj C ) → Obj C
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
166 _⊗_ x y = (IsMonoidal._□_ (Monoidal.isMonoidal M) ) x y
704
b48c2d1c0796 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 703
diff changeset
167 _□_ : {a b c d : Obj C } ( f : Hom C a c ) ( g : Hom C b d ) → Hom C ( a ⊗ b ) ( c ⊗ d )
b48c2d1c0796 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 703
diff changeset
168 _□_ f g = FMap (Monoidal.m-bi M) ( f , g )
b48c2d1c0796 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 703
diff changeset
169 F : { a b : Obj C } → ( f : Hom C a b ) → Hom D (FObj MF a) (FObj MF b )
b48c2d1c0796 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 703
diff changeset
170 F f = FMap MF f
703
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
171 ≈-cong : {a b : Obj (C × C)} {f g : Hom (C × C) a b} → (C × C) [ f ≈ g ] →
704
b48c2d1c0796 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 703
diff changeset
172 D [ F ( (proj₁ f □ proj₂ f)) ≈ F ( (proj₁ g □ proj₂ g)) ]
703
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
173 ≈-cong {a} {b} {f} {g} f≈g = IsFunctor.≈-cong (isFunctor MF ) ( IsFunctor.≈-cong (isFunctor (Monoidal.m-bi M) ) f≈g )
704
b48c2d1c0796 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 703
diff changeset
174 identity : {a : Obj (C × C)} → D [ F ( (proj₁ (id1 (C × C) a) □ proj₂ (id1 (C × C) a)))
703
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
175 ≈ id1 D (FObj MF (proj₁ a ⊗ proj₂ a)) ]
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
176 identity {a} = let open ≈-Reasoning D in begin
704
b48c2d1c0796 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 703
diff changeset
177 F ( (proj₁ (id1 (C × C) a) □ proj₂ (id1 (C × C) a)))
703
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
178 ≈⟨⟩
704
b48c2d1c0796 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 703
diff changeset
179 F (FMap (Monoidal.m-bi M) (id1 (C × C) a ) )
703
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
180 ≈⟨ fcong MF ( IsFunctor.identity (isFunctor (Monoidal.m-bi M) )) ⟩
704
b48c2d1c0796 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 703
diff changeset
181 F (id1 C (proj₁ a ⊗ proj₂ a))
703
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
182 ≈⟨ IsFunctor.identity (isFunctor MF) ⟩
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
183 id1 D (FObj MF (proj₁ a ⊗ proj₂ a))
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
184 ∎
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
185 distr : {a b c : Obj (C × C)} {f : Hom (C × C) a b} {g : Hom (C × C) b c} → D [
704
b48c2d1c0796 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 703
diff changeset
186 F ( (proj₁ ((C × C) [ g o f ]) □ proj₂ ((C × C) [ g o f ])))
b48c2d1c0796 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 703
diff changeset
187 ≈ D [ F ( (proj₁ g □ proj₂ g)) o F ( (proj₁ f □ proj₂ f)) ] ]
703
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
188 distr {a} {b} {c} {f} {g} = let open ≈-Reasoning D in begin
704
b48c2d1c0796 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 703
diff changeset
189 F ( (proj₁ ((C × C) [ g o f ]) □ proj₂ ((C × C) [ g o f ])))
703
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
190 ≈⟨⟩
704
b48c2d1c0796 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 703
diff changeset
191 F (FMap (Monoidal.m-bi M) ( (C × C) [ g o f ] ))
703
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
192 ≈⟨ fcong MF ( IsFunctor.distr (isFunctor (Monoidal.m-bi M))) ⟩
704
b48c2d1c0796 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 703
diff changeset
193 F (C [ FMap (Monoidal.m-bi M) g o FMap (Monoidal.m-bi M) f ])
703
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
194 ≈⟨ IsFunctor.distr ( isFunctor MF ) ⟩
704
b48c2d1c0796 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 703
diff changeset
195 F ( proj₁ g □ proj₂ g) o F ( proj₁ f □ proj₂ f)
703
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
196 ∎
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
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
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
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
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
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
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
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
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
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
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
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
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
217 open Iso
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
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
10ab28030c20 add definitions
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 698
diff changeset
220 αC : {a b c : Obj C} → Hom C (( a ⊗ b ) ⊗ c ) ( a ⊗ ( b ⊗ c ) )
10ab28030c20 add definitions
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 698
diff changeset
221 αC {a} {b} {c} = ≅→ (mα-iso (isMonoidal M) {a} {b} {c})
10ab28030c20 add definitions
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 698
diff changeset
222 αD : {a b c : Obj D} → Hom D (( a ● b ) ● c ) ( a ● ( b ● c ) )
10ab28030c20 add definitions
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 698
diff changeset
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 -----
117e5b392673 Generalize Free Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 730
diff changeset
267 -- they say it is not possible to prove FreeTheorem in Agda nor Coq
117e5b392673 Generalize Free Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 730
diff changeset
268 -- https://stackoverflow.com/questions/24718567/is-it-possible-to-get-hold-of-free-theorems-as-propositional-equalities
117e5b392673 Generalize Free Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 730
diff changeset
269 -- so we postulate this
117e5b392673 Generalize Free Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 730
diff changeset
270 -- and we cannot indent postulate ...
117e5b392673 Generalize Free Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 730
diff changeset
271 postulate FreeTheorem : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (C : Category c₁ c₂ ℓ) (D : Category c₁' c₂' ℓ') {a b c : Obj C } → (F : Functor C D ) → ( fmap : {a : Obj C } {b : Obj C } → Hom C a b → Hom D (FObj F a) ( FObj F b) ) → {h f : Hom C a b } → {g k : Hom C b c } → C [ C [ g o h ] ≈ C [ k o f ] ] → D [ D [ FMap F g o fmap h ] ≈ D [ fmap k o FMap F f ] ]
732
2439a142aba2 add Monad to Monoidal Functor / Applicative
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 731
diff changeset
272
731
117e5b392673 Generalize Free Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 730
diff changeset
273 UniquenessOfFunctor : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (C : Category c₁ c₂ ℓ) (D : Category c₁' c₂' ℓ') (F : Functor C D)
117e5b392673 Generalize Free Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 730
diff changeset
274 {a b : Obj C } { f : Hom C a b } → ( fmap : {a : Obj C } {b : Obj C } → Hom C a b → Hom D (FObj F a) ( FObj F b) )
117e5b392673 Generalize Free Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 730
diff changeset
275 → ( {b : Obj C } → D [ fmap (id1 C b) ≈ id1 D (FObj F b) ] )
117e5b392673 Generalize Free Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 730
diff changeset
276 → D [ fmap f ≈ FMap F f ]
117e5b392673 Generalize Free Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 730
diff changeset
277 UniquenessOfFunctor C D F {a} {b} {f} fmap eq = begin
117e5b392673 Generalize Free Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 730
diff changeset
278 fmap f
117e5b392673 Generalize Free Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 730
diff changeset
279 ≈↑⟨ idL ⟩
117e5b392673 Generalize Free Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 730
diff changeset
280 id1 D (FObj F b) o fmap f
117e5b392673 Generalize Free Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 730
diff changeset
281 ≈↑⟨ car ( IsFunctor.identity (isFunctor F )) ⟩
117e5b392673 Generalize Free Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 730
diff changeset
282 FMap F (id1 C b) o fmap f
117e5b392673 Generalize Free Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 730
diff changeset
283 ≈⟨ FreeTheorem C D F fmap (IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory C ))) ⟩
117e5b392673 Generalize Free Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 730
diff changeset
284 fmap (id1 C b) o FMap F f
117e5b392673 Generalize Free Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 730
diff changeset
285 ≈⟨ car eq ⟩
117e5b392673 Generalize Free Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 730
diff changeset
286 id1 D (FObj F b) o FMap F f
117e5b392673 Generalize Free Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 730
diff changeset
287 ≈⟨ idL ⟩
117e5b392673 Generalize Free Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 730
diff changeset
288 FMap F f
117e5b392673 Generalize Free Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 730
diff changeset
289 ∎
117e5b392673 Generalize Free Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 730
diff changeset
290 where open ≈-Reasoning D
117e5b392673 Generalize Free Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 730
diff changeset
291
705
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
292 open import Category.Sets
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
293
706
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 705
diff changeset
294 import Relation.Binary.PropositionalEquality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 705
diff changeset
295 -- 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 )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 705
diff changeset
296 postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 705
diff changeset
297
730
e4ef69bae044 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 729
diff changeset
298 ------
e4ef69bae044 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 729
diff changeset
299 -- Data.Product as a Tensor Product for Monoidal Category
e4ef69bae044 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 729
diff changeset
300 --
705
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
301
708
975aa343a963 Sets is Monoidal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 707
diff changeset
302 SetsTensorProduct : {c : Level} → Functor ( Sets {c} × Sets {c} ) (Sets {c})
975aa343a963 Sets is Monoidal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 707
diff changeset
303 SetsTensorProduct = record {
975aa343a963 Sets is Monoidal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 707
diff changeset
304 FObj = λ x → proj₁ x * proj₂ x
975aa343a963 Sets is Monoidal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 707
diff changeset
305 ; FMap = λ {x : Obj ( Sets × Sets ) } {y} f → map (proj₁ f) (proj₂ f)
975aa343a963 Sets is Monoidal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 707
diff changeset
306 ; isFunctor = record {
975aa343a963 Sets is Monoidal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 707
diff changeset
307 ≈-cong = ≈-cong
975aa343a963 Sets is Monoidal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 707
diff changeset
308 ; identity = refl
975aa343a963 Sets is Monoidal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 707
diff changeset
309 ; distr = refl
706
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 705
diff changeset
310 }
708
975aa343a963 Sets is Monoidal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 707
diff changeset
311 } where
975aa343a963 Sets is Monoidal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 707
diff changeset
312 ≈-cong : {a b : Obj (Sets × Sets)} {f g : Hom (Sets × Sets) a b} →
975aa343a963 Sets is Monoidal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 707
diff changeset
313 (Sets × Sets) [ f ≈ g ] → Sets [ map (proj₁ f) (proj₂ f) ≈ map (proj₁ g) (proj₂ g) ]
975aa343a963 Sets is Monoidal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 707
diff changeset
314 ≈-cong (refl , refl) = refl
975aa343a963 Sets is Monoidal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 707
diff changeset
315
730
e4ef69bae044 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 729
diff changeset
316 -----
e4ef69bae044 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 729
diff changeset
317 --
e4ef69bae044 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 729
diff changeset
318 -- Sets as Monoidal Category
e4ef69bae044 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 729
diff changeset
319 --
e4ef69bae044 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 729
diff changeset
320 -- almost all comutativities are refl
e4ef69bae044 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 729
diff changeset
321 --
e4ef69bae044 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 729
diff changeset
322 --
e4ef69bae044 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 729
diff changeset
323 --
708
975aa343a963 Sets is Monoidal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 707
diff changeset
324
730
e4ef69bae044 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 729
diff changeset
325 data One {c : Level} : Set c where
e4ef69bae044 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 729
diff changeset
326 OneObj : One -- () in Haskell ( or any one object set )
708
975aa343a963 Sets is Monoidal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 707
diff changeset
327
975aa343a963 Sets is Monoidal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 707
diff changeset
328 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
329 MonoidalSets {c} = record {
ea84cc6c1797 monoidal functor and applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 726
diff changeset
330 m-i = One {c} ;
708
975aa343a963 Sets is Monoidal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 707
diff changeset
331 m-bi = SetsTensorProduct ;
975aa343a963 Sets is Monoidal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 707
diff changeset
332 isMonoidal = record {
975aa343a963 Sets is Monoidal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 707
diff changeset
333 mα-iso = record { ≅→ = mα→ ; ≅← = mα← ; iso→ = refl ; iso← = refl } ;
975aa343a963 Sets is Monoidal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 707
diff changeset
334 mλ-iso = record { ≅→ = mλ→ ; ≅← = mλ← ; iso→ = extensionality Sets ( λ x → mλiso x ) ; iso← = refl } ;
975aa343a963 Sets is Monoidal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 707
diff changeset
335 mρ-iso = record { ≅→ = mρ→ ; ≅← = mρ← ; iso→ = extensionality Sets ( λ x → mρiso x ) ; iso← = refl } ;
975aa343a963 Sets is Monoidal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 707
diff changeset
336 mα→nat1 = λ f → refl ;
975aa343a963 Sets is Monoidal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 707
diff changeset
337 mα→nat2 = λ f → refl ;
975aa343a963 Sets is Monoidal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 707
diff changeset
338 mα→nat3 = λ f → refl ;
975aa343a963 Sets is Monoidal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 707
diff changeset
339 mλ→nat = λ f → refl ;
975aa343a963 Sets is Monoidal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 707
diff changeset
340 mρ→nat = λ f → refl ;
975aa343a963 Sets is Monoidal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 707
diff changeset
341 comm-penta = refl ;
975aa343a963 Sets is Monoidal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 707
diff changeset
342 comm-unit = refl
975aa343a963 Sets is Monoidal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 707
diff changeset
343 }
975aa343a963 Sets is Monoidal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 707
diff changeset
344 } where
975aa343a963 Sets is Monoidal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 707
diff changeset
345 _⊗_ : ( a b : Obj Sets ) → Obj Sets
975aa343a963 Sets is Monoidal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 707
diff changeset
346 _⊗_ a b = FObj SetsTensorProduct (a , b )
730
e4ef69bae044 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 729
diff changeset
347 -- association operations
708
975aa343a963 Sets is Monoidal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 707
diff changeset
348 mα→ : {a b c : Obj Sets} → Hom Sets ( ( a ⊗ b ) ⊗ c ) ( a ⊗ ( b ⊗ c ) )
975aa343a963 Sets is Monoidal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 707
diff changeset
349 mα→ ((a , b) , c ) = (a , ( b , c ) )
975aa343a963 Sets is Monoidal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 707
diff changeset
350 mα← : {a b c : Obj Sets} → Hom Sets ( a ⊗ ( b ⊗ c ) ) ( ( a ⊗ b ) ⊗ c )
975aa343a963 Sets is Monoidal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 707
diff changeset
351 mα← (a , ( b , c ) ) = ((a , b) , c )
730
e4ef69bae044 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 729
diff changeset
352 -- (One , a) ⇔ a
708
975aa343a963 Sets is Monoidal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 707
diff changeset
353 mλ→ : {a : Obj Sets} → Hom Sets ( One ⊗ a ) a
975aa343a963 Sets is Monoidal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 707
diff changeset
354 mλ→ (_ , a) = a
975aa343a963 Sets is Monoidal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 707
diff changeset
355 mλ← : {a : Obj Sets} → Hom Sets a ( One ⊗ a )
975aa343a963 Sets is Monoidal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 707
diff changeset
356 mλ← a = ( OneObj , a )
975aa343a963 Sets is Monoidal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 707
diff changeset
357 mλiso : {a : Obj Sets} (x : One ⊗ a) → (Sets [ mλ← o mλ→ ]) x ≡ id1 Sets (One ⊗ a) x
975aa343a963 Sets is Monoidal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 707
diff changeset
358 mλiso (OneObj , _ ) = refl
730
e4ef69bae044 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 729
diff changeset
359 -- (a , One) ⇔ a
708
975aa343a963 Sets is Monoidal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 707
diff changeset
360 mρ→ : {a : Obj Sets} → Hom Sets ( a ⊗ One ) a
975aa343a963 Sets is Monoidal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 707
diff changeset
361 mρ→ (a , _) = a
975aa343a963 Sets is Monoidal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 707
diff changeset
362 mρ← : {a : Obj Sets} → Hom Sets a ( a ⊗ One )
975aa343a963 Sets is Monoidal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 707
diff changeset
363 mρ← a = ( a , OneObj )
975aa343a963 Sets is Monoidal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 707
diff changeset
364 mρiso : {a : Obj Sets} (x : a ⊗ One ) → (Sets [ mρ← o mρ→ ]) x ≡ id1 Sets (a ⊗ One) x
975aa343a963 Sets is Monoidal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 707
diff changeset
365 mρiso (_ , OneObj ) = refl
975aa343a963 Sets is Monoidal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 707
diff changeset
366
710
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 709
diff changeset
367 ≡-cong = Relation.Binary.PropositionalEquality.cong
706
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 705
diff changeset
368
713
5e101ee6dab9 identity done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 712
diff changeset
369
5e101ee6dab9 identity done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 712
diff changeset
370 record IsHaskellMonoidalFunctor {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) )
5e101ee6dab9 identity done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 712
diff changeset
371 ( unit : FObj F One )
5e101ee6dab9 identity done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 712
diff changeset
372 ( φ : {a b : Obj Sets} → Hom Sets ((FObj F a) * (FObj F b )) ( FObj F ( a * b ) ) )
5e101ee6dab9 identity done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 712
diff changeset
373 : Set (suc (suc c₁)) where
5e101ee6dab9 identity done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 712
diff changeset
374 isM : IsMonoidal (Sets {c₁}) One SetsTensorProduct
5e101ee6dab9 identity done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 712
diff changeset
375 isM = Monoidal.isMonoidal MonoidalSets
5e101ee6dab9 identity done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 712
diff changeset
376 open IsMonoidal
5e101ee6dab9 identity done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 712
diff changeset
377 field
715
1be42267eeee add some tools
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 714
diff changeset
378 natφ : { a b c d : Obj Sets } { x : FObj F a} { y : FObj F b} { f : a → c } { g : b → d }
713
5e101ee6dab9 identity done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 712
diff changeset
379 → FMap F (map f g) (φ (x , y)) ≡ φ (FMap F f x , FMap F g y)
715
1be42267eeee add some tools
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 714
diff changeset
380 assocφ : { x y z : Obj Sets } { a : FObj F x } { b : FObj F y }{ c : FObj F z }
713
5e101ee6dab9 identity done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 712
diff changeset
381 → φ (a , φ (b , c)) ≡ FMap F (Iso.≅→ (mα-iso isM)) (φ (φ (a , b) , c))
715
1be42267eeee add some tools
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 714
diff changeset
382 idrφ : {a : Obj Sets } { x : FObj F a } → FMap F (Iso.≅→ (mρ-iso isM)) (φ (x , unit)) ≡ x
1be42267eeee add some tools
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 714
diff changeset
383 idlφ : {a : Obj Sets } { x : FObj F a } → FMap F (Iso.≅→ (mλ-iso isM)) (φ (unit , x)) ≡ x
713
5e101ee6dab9 identity done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 712
diff changeset
384
714
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 713
diff changeset
385 -- http://www.staff.city.ac.uk/~ross/papers/Applicative.pdf
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 713
diff changeset
386 -- naturality of φ fmap(f × g)(φ u v) = φ ( fmap f u) ( fmap g v )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 713
diff changeset
387 -- left identity fmap snd (φ unit v) = v
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 713
diff changeset
388 -- right identity fmap fst (φ u unit) = u
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 713
diff changeset
389 -- associativity fmap assoc (φ u (φ v w)) = φ (φ u v) w
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 713
diff changeset
390
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 713
diff changeset
391
730
e4ef69bae044 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 729
diff changeset
392 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
393 : Set (suc (suc c₁)) where
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
394 field
730
e4ef69bae044 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 729
diff changeset
395 unit : FObj F One
e4ef69bae044 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 729
diff changeset
396 φ : {a b : Obj Sets} → Hom Sets ((FObj F a) * (FObj F b )) ( FObj F ( a * b ) )
766
c30ca91f3a76 Applicative all done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 765
diff changeset
397 isHaskellMonoidalFunctor : IsHaskellMonoidalFunctor F unit φ
705
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
398
730
e4ef69bae044 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 729
diff changeset
399 HaskellMonoidalFunctor→MonoidalFunctor : {c : Level} ( F : Functor (Sets {c}) (Sets {c}) ) → (mf : HaskellMonoidalFunctor F )
713
5e101ee6dab9 identity done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 712
diff changeset
400 → MonoidalFunctor {_} {c} {_} {Sets} {Sets} MonoidalSets MonoidalSets
766
c30ca91f3a76 Applicative all done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 765
diff changeset
401 HaskellMonoidalFunctor→MonoidalFunctor {c} F mf = record {
709
2807335e3fa0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 708
diff changeset
402 MF = F
2807335e3fa0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 708
diff changeset
403 ; ψ = λ _ → HaskellMonoidalFunctor.unit mf
2807335e3fa0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 708
diff changeset
404 ; isMonodailFunctor = record {
711
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 710
diff changeset
405 φab = record { TMap = λ x → φ ; isNTrans = record { commute = comm0 } }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 710
diff changeset
406 ; associativity = λ {a b c} → comm1 {a} {b} {c}
710
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 709
diff changeset
407 ; unitarity-idr = λ {a b} → comm2 {a} {b}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 709
diff changeset
408 ; unitarity-idl = λ {a b} → comm3 {a} {b}
709
2807335e3fa0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 708
diff changeset
409 }
2807335e3fa0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 708
diff changeset
410 } where
2807335e3fa0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 708
diff changeset
411 open Monoidal
2807335e3fa0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 708
diff changeset
412 open IsMonoidal hiding ( _■_ ; _□_ )
766
c30ca91f3a76 Applicative all done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 765
diff changeset
413 ismf : IsHaskellMonoidalFunctor F ( HaskellMonoidalFunctor.unit mf ) ( HaskellMonoidalFunctor.φ mf )
c30ca91f3a76 Applicative all done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 765
diff changeset
414 ismf = HaskellMonoidalFunctor.isHaskellMonoidalFunctor mf
730
e4ef69bae044 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 729
diff changeset
415 M : Monoidal (Sets {c})
709
2807335e3fa0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 708
diff changeset
416 M = MonoidalSets
730
e4ef69bae044 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 729
diff changeset
417 isM : IsMonoidal (Sets {c}) One SetsTensorProduct
709
2807335e3fa0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 708
diff changeset
418 isM = Monoidal.isMonoidal MonoidalSets
730
e4ef69bae044 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 729
diff changeset
419 unit : FObj F One
709
2807335e3fa0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 708
diff changeset
420 unit = HaskellMonoidalFunctor.unit mf
2807335e3fa0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 708
diff changeset
421 _⊗_ : (x y : Obj Sets ) → Obj Sets
2807335e3fa0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 708
diff changeset
422 _⊗_ x y = (IsMonoidal._□_ (Monoidal.isMonoidal M) ) x y
2807335e3fa0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 708
diff changeset
423 _□_ : {a b c d : Obj Sets } ( f : Hom Sets a c ) ( g : Hom Sets b d ) → Hom Sets ( a ⊗ b ) ( c ⊗ d )
2807335e3fa0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 708
diff changeset
424 _□_ f g = FMap (m-bi M) ( f , g )
711
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 710
diff changeset
425 φ : {x : Obj (Sets × Sets) } → Hom Sets (FObj (Functor● Sets Sets MonoidalSets F) x) (FObj (Functor⊗ Sets Sets MonoidalSets F) x)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 710
diff changeset
426 φ z = HaskellMonoidalFunctor.φ mf z
710
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 709
diff changeset
427 comm00 : {a b : Obj (Sets × Sets)} { f : Hom (Sets × Sets) a b} (x : ( FObj F (proj₁ a) * FObj F (proj₂ a)) ) →
711
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 710
diff changeset
428 (Sets [ FMap (Functor⊗ Sets Sets MonoidalSets F) f o φ ]) x ≡ (Sets [ φ o FMap (Functor● Sets Sets MonoidalSets F) f ]) x
710
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 709
diff changeset
429 comm00 {a} {b} {(f , g)} (x , y) = begin
711
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 710
diff changeset
430 (FMap (Functor⊗ Sets Sets MonoidalSets F) (f , g) ) (φ (x , y))
710
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 709
diff changeset
431 ≡⟨⟩
711
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 710
diff changeset
432 (FMap F ( f □ g ) ) (φ (x , y))
710
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 709
diff changeset
433 ≡⟨⟩
711
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 710
diff changeset
434 FMap F ( map f g ) (φ (x , y))
715
1be42267eeee add some tools
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 714
diff changeset
435 ≡⟨ IsHaskellMonoidalFunctor.natφ ismf ⟩
711
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 710
diff changeset
436 φ ( FMap F f x , FMap F g y )
710
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 709
diff changeset
437 ≡⟨⟩
711
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 710
diff changeset
438 φ ( ( FMap F f □ FMap F g ) (x , y) )
710
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 709
diff changeset
439 ≡⟨⟩
711
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 710
diff changeset
440 φ ((FMap (Functor● Sets Sets MonoidalSets F) (f , g) ) (x , y) )
710
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 709
diff changeset
441 ∎
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 709
diff changeset
442 where
713
5e101ee6dab9 identity done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 712
diff changeset
443 open Relation.Binary.PropositionalEquality.≡-Reasoning
711
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 710
diff changeset
444 comm0 : {a b : Obj (Sets × Sets)} { f : Hom (Sets × Sets) a b} → Sets [ Sets [ FMap (Functor⊗ Sets Sets MonoidalSets F) f o φ ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 710
diff changeset
445 ≈ Sets [ φ o FMap (Functor● Sets Sets MonoidalSets F) f ] ]
710
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 709
diff changeset
446 comm0 {a} {b} {f} = extensionality Sets ( λ (x : ( FObj F (proj₁ a) * FObj F (proj₂ a)) ) → comm00 x )
711
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 710
diff changeset
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 ≡
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 710
diff changeset
448 (Sets [ FMap F (Iso.≅→ (mα-iso isM)) o Sets [ φ o φ □ id1 Sets (FObj F c) ] ]) x
710
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 709
diff changeset
449 comm10 {x} {y} {f} ((a , b) , c ) = begin
711
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 710
diff changeset
450 φ (( id1 Sets (FObj F x) □ φ ) ( ( Iso.≅→ (mα-iso isM) ) ((a , b) , c)))
710
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 709
diff changeset
451 ≡⟨⟩
711
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 710
diff changeset
452 φ ( a , φ (b , c))
715
1be42267eeee add some tools
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 714
diff changeset
453 ≡⟨ IsHaskellMonoidalFunctor.assocφ ismf ⟩
711
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 710
diff changeset
454 ( FMap F (Iso.≅→ (mα-iso isM))) (φ (( φ (a , b)) , c ))
710
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 709
diff changeset
455 ≡⟨⟩
711
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 710
diff changeset
456 ( FMap F (Iso.≅→ (mα-iso isM))) (φ (( φ □ id1 Sets (FObj F f) ) ((a , b) , c)))
710
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 709
diff changeset
457 ∎
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 709
diff changeset
458 where
713
5e101ee6dab9 identity done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 712
diff changeset
459 open Relation.Binary.PropositionalEquality.≡-Reasoning
711
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 710
diff changeset
460 comm1 : {a b c : Obj Sets} → Sets [ Sets [ φ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 710
diff changeset
461 o Sets [ (id1 Sets (FObj F a) □ φ ) o Iso.≅→ (mα-iso isM) ] ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 710
diff changeset
462 ≈ Sets [ FMap F (Iso.≅→ (mα-iso isM)) o Sets [ φ o (φ □ id1 Sets (FObj F c)) ] ] ]
710
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 709
diff changeset
463 comm1 {a} {b} {c} = extensionality Sets ( λ x → comm10 x )
712
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 711
diff changeset
464 comm20 : {a b : Obj Sets} ( x : FObj F a * One ) → ( Sets [
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 711
diff changeset
465 FMap F (Iso.≅→ (mρ-iso isM)) o Sets [ φ o
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 711
diff changeset
466 FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit )) ] ] ) x ≡ Iso.≅→ (mρ-iso isM) x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 711
diff changeset
467 comm20 {a} {b} (x , OneObj ) = begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 711
diff changeset
468 (FMap F (Iso.≅→ (mρ-iso isM))) ( φ ( x , unit ) )
715
1be42267eeee add some tools
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 714
diff changeset
469 ≡⟨ IsHaskellMonoidalFunctor.idrφ ismf ⟩
712
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 711
diff changeset
470 x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 711
diff changeset
471 ≡⟨⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 711
diff changeset
472 Iso.≅→ (mρ-iso isM) ( x , OneObj )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 711
diff changeset
473 ∎
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 711
diff changeset
474 where
713
5e101ee6dab9 identity done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 712
diff changeset
475 open Relation.Binary.PropositionalEquality.≡-Reasoning
709
2807335e3fa0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 708
diff changeset
476 comm2 : {a b : Obj Sets} → Sets [ Sets [
711
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 710
diff changeset
477 FMap F (Iso.≅→ (mρ-iso isM)) o Sets [ φ o
709
2807335e3fa0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 708
diff changeset
478 FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit )) ] ] ≈ Iso.≅→ (mρ-iso isM) ]
712
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 711
diff changeset
479 comm2 {a} {b} = extensionality Sets ( λ x → comm20 {a} {b} x )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 711
diff changeset
480 comm30 : {a b : Obj Sets} ( x : One * FObj F b ) → ( Sets [
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 711
diff changeset
481 FMap F (Iso.≅→ (mλ-iso isM)) o Sets [ φ o
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 711
diff changeset
482 FMap (m-bi MonoidalSets) ((λ _ → unit ) , id1 Sets (FObj F b) ) ] ] ) x ≡ Iso.≅→ (mλ-iso isM) x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 711
diff changeset
483 comm30 {a} {b} ( OneObj , x) = begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 711
diff changeset
484 (FMap F (Iso.≅→ (mλ-iso isM))) ( φ ( unit , x ) )
715
1be42267eeee add some tools
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 714
diff changeset
485 ≡⟨ IsHaskellMonoidalFunctor.idlφ ismf ⟩
712
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 711
diff changeset
486 x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 711
diff changeset
487 ≡⟨⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 711
diff changeset
488 Iso.≅→ (mλ-iso isM) ( OneObj , x )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 711
diff changeset
489 ∎
711
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 710
diff changeset
490 where
713
5e101ee6dab9 identity done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 712
diff changeset
491 open Relation.Binary.PropositionalEquality.≡-Reasoning
709
2807335e3fa0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 708
diff changeset
492 comm3 : {a b : Obj Sets} → Sets [ Sets [ FMap F (Iso.≅→ (mλ-iso isM)) o
711
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 710
diff changeset
493 Sets [ φ o FMap (m-bi MonoidalSets) ((λ _ → unit ) , id1 Sets (FObj F b)) ] ] ≈ Iso.≅→ (mλ-iso isM) ]
712
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 711
diff changeset
494 comm3 {a} {b} = extensionality Sets ( λ x → comm30 {a} {b} x )
709
2807335e3fa0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 708
diff changeset
495
705
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
496