Mercurial > hg > Members > kono > Proof > category
annotate monoidal.agda @ 703:df3f1aae984f
Monidal functor done.
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 22 Nov 2017 04:12:14 +0900 |
parents | d16327b48b83 |
children | b48c2d1c0796 |
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 Level |
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
3 open import Level |
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
4 open import Category |
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
5 module monoidal where |
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
6 |
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
7 open import Data.Product renaming (_×_ to _*_) |
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
8 open import Category.Constructions.Product |
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
9 open import HomReasoning |
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
10 open import cat-utility |
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
11 open import Relation.Binary.Core |
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
12 open import Relation.Binary |
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
13 |
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
14 open Functor |
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
15 |
698 | 16 record Iso {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ) |
17 (x y : Obj C ) | |
18 : Set ( suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where | |
696
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
19 field |
698 | 20 ≅→ : Hom C x y |
21 ≅← : Hom C y x | |
22 iso→ : C [ C [ ≅← o ≅→ ] ≈ id1 C x ] | |
23 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
|
24 |
698 | 25 record IsStrictMonoidal {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ) (I : Obj C) ( BI : Functor ( C × C ) C ) |
696
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
26 : Set ( suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where |
700
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
27 infixr 9 _□_ |
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
28 _□_ : ( x y : Obj C ) → Obj C |
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
29 _□_ x y = FObj BI ( x , y ) |
696
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
30 field |
700
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
31 mα : {a b c : Obj C} → ( a □ b) □ c ≡ a □ ( b □ c ) |
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
32 mλ : (a : Obj C) → I □ a ≡ a |
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
33 mρ : (a : Obj C) → a □ I ≡ a |
698 | 34 |
35 record StrictMonoidal {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ) | |
36 : Set ( suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where | |
37 field | |
38 m-i : Obj C | |
39 m-bi : Functor ( C × C ) C | |
40 isMonoidal : IsStrictMonoidal C m-i m-bi | |
41 | |
696
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
42 |
698 | 43 -- non strict version includes 5 naturalities |
44 record IsMonoidal {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ) (I : Obj C) ( BI : Functor ( C × C ) C ) | |
45 : Set ( suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where | |
46 open Iso | |
700
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
47 infixr 9 _□_ _■_ |
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
48 _□_ : ( x y : Obj C ) → Obj C |
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
49 _□_ x y = FObj BI ( x , y ) |
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
50 _■_ : {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
|
51 _■_ f g = FMap BI ( f , g ) |
698 | 52 field |
700
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
53 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
|
54 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
|
55 mρ-iso : {a : Obj C} → Iso C ( a □ I) a |
698 | 56 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
|
57 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
|
58 C [ ≅→ (mα-iso ) o ( (f ■ id1 C b ) ■ id1 C c ) ] ] |
698 | 59 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
|
60 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
|
61 C [ ≅→ (mα-iso ) o ( (id1 C a ■ f ) ■ id1 C c ) ] ] |
698 | 62 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
|
63 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
|
64 C [ ≅→ (mα-iso ) o ( id1 C ( a □ b ) ■ f ) ] ] |
698 | 65 mλ→nat : {a a' : Obj C} → ( f : Hom C a a' ) → |
66 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
|
67 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
|
68 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
|
69 C [ C [ f o ≅→ (mρ-iso {a} ) ] ≈ |
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
70 C [ ≅→ (mρ-iso ) o ( f ■ id1 C I ) ] ] |
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
71 α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
|
72 α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
|
73 α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
|
74 α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
|
75 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
|
76 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
|
77 α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
|
78 α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
|
79 α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
|
80 α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
|
81 α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
|
82 αAIB {a} {b} = ≅→ mα-iso |
700
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
83 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
|
84 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
|
85 ρ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
|
86 ρ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
|
87 |
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
88 field |
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
89 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
|
90 → 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
|
91 ≈ αA□BCD {a} {b} {c} {d} {e} ] |
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
92 comm-unit : {a b : Obj C} |
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
93 → 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
|
94 |
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
95 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
|
96 : Set ( suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where |
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
97 field |
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
98 m-i : Obj C |
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
99 m-bi : Functor ( C × C ) C |
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
100 isMonoidal : IsMonoidal C m-i m-bi |
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
101 |
703 | 102 Functor● : {c₁ c₂ ℓ : Level} (C D : Category c₁ c₂ ℓ) ( N : Monoidal D ) |
103 ( MF : Functor C D ) → Functor ( C × C ) D | |
104 Functor● C D N MF = record { | |
105 FObj = λ x → (FObj MF (proj₁ x) ) ● (FObj MF (proj₂ x) ) | |
106 ; FMap = λ {x : Obj ( C × C ) } {y} f → FMap (Monoidal.m-bi N) ( FMap MF (proj₁ f ) , FMap MF (proj₂ f) ) | |
107 ; isFunctor = record { | |
108 ≈-cong = ≈-cong | |
109 ; identity = identity | |
110 ; distr = distr | |
111 } | |
112 } where | |
113 _●_ : (x y : Obj D ) → Obj D | |
114 _●_ x y = (IsMonoidal._□_ (Monoidal.isMonoidal N) ) x y | |
115 ≈-cong : {a b : Obj (C × C)} {f g : Hom (C × C) a b} → (C × C) [ f ≈ g ] → | |
116 D [ FMap (Monoidal.m-bi N) (FMap MF (proj₁ f) , FMap MF (proj₂ f)) | |
117 ≈ FMap (Monoidal.m-bi N) (FMap MF (proj₁ g) , FMap MF (proj₂ g)) ] | |
118 ≈-cong {a} {b} {f} {g} f≈g = let open ≈-Reasoning D in begin | |
119 FMap (Monoidal.m-bi N) (FMap MF (proj₁ f) , FMap MF (proj₂ f)) | |
120 ≈⟨ fcong (Monoidal.m-bi N) ( fcong MF ( proj₁ f≈g ) , fcong MF ( proj₂ f≈g )) ⟩ | |
121 FMap (Monoidal.m-bi N) (FMap MF (proj₁ g) , FMap MF (proj₂ g)) | |
122 ∎ | |
123 identity : {a : Obj (C × C)} → D [ FMap (Monoidal.m-bi N) (FMap MF (proj₁ (id1 (C × C) a)) , FMap MF (proj₂ (id1 (C × C) a))) | |
124 ≈ id1 D (FObj MF (proj₁ a) ● FObj MF (proj₂ a)) ] | |
125 identity {a} = let open ≈-Reasoning D in begin | |
126 FMap (Monoidal.m-bi N) (FMap MF (proj₁ (id1 (C × C) a)) , FMap MF (proj₂ (id1 (C × C) a))) | |
127 ≈⟨ fcong (Monoidal.m-bi N) ( IsFunctor.identity (isFunctor MF ) , IsFunctor.identity (isFunctor MF )) ⟩ | |
128 FMap (Monoidal.m-bi N) ( id1 D (FObj MF (proj₁ a)) , id1 D (FObj MF (proj₂ a))) | |
129 ≈⟨ IsFunctor.identity (isFunctor (Monoidal.m-bi N)) ⟩ | |
130 id1 D (FObj MF (proj₁ a) ● FObj MF (proj₂ a)) | |
131 ∎ | |
132 distr : {a b c : Obj (C × C)} {f : Hom (C × C) a b} {g : Hom (C × C) b c} → | |
133 D [ FMap (Monoidal.m-bi N) (FMap MF (proj₁ ((C × C) [ g o f ])) , FMap MF (proj₂ ((C × C) [ g o f ]))) | |
134 ≈ D [ FMap (Monoidal.m-bi N) (FMap MF (proj₁ g) , FMap MF (proj₂ g)) o FMap (Monoidal.m-bi N) (FMap MF (proj₁ f) , FMap MF (proj₂ f)) ] ] | |
135 distr {a} {b} {c} {f} {g} = let open ≈-Reasoning D in begin | |
136 FMap (Monoidal.m-bi N) (FMap MF (proj₁ ((C × C) [ g o f ])) , FMap MF (proj₂ ((C × C) [ g o f ]))) | |
137 ≈⟨ fcong (Monoidal.m-bi N) ( IsFunctor.distr ( isFunctor MF) , IsFunctor.distr ( isFunctor MF )) ⟩ | |
138 FMap (Monoidal.m-bi N) ( D [ FMap MF (proj₁ g) o FMap MF (proj₁ f) ] , D [ FMap MF (proj₂ g) o FMap MF (proj₂ f) ] ) | |
139 ≈⟨ IsFunctor.distr ( isFunctor (Monoidal.m-bi N)) ⟩ | |
140 FMap (Monoidal.m-bi N) (FMap MF (proj₁ g) , FMap MF (proj₂ g)) o FMap (Monoidal.m-bi N) (FMap MF (proj₁ f) , FMap MF (proj₂ f)) | |
141 ∎ | |
696
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
142 |
703 | 143 Functor⊗ : {c₁ c₂ ℓ : Level} (C D : Category c₁ c₂ ℓ) ( M : Monoidal C ) |
144 ( MF : Functor C D ) → Functor ( C × C ) D | |
145 Functor⊗ C D M MF = record { | |
146 FObj = λ x → FObj MF ( proj₁ x ⊗ proj₂ x ) | |
147 ; FMap = λ {a} {b} f → FMap MF ( FMap (Monoidal.m-bi M) ( proj₁ f , proj₂ f) ) | |
148 ; isFunctor = record { | |
149 ≈-cong = ≈-cong | |
150 ; identity = identity | |
151 ; distr = distr | |
152 } | |
153 } where | |
154 _⊗_ : (x y : Obj C ) → Obj C | |
155 _⊗_ x y = (IsMonoidal._□_ (Monoidal.isMonoidal M) ) x y | |
156 ≈-cong : {a b : Obj (C × C)} {f g : Hom (C × C) a b} → (C × C) [ f ≈ g ] → | |
157 D [ FMap MF (FMap (Monoidal.m-bi M) (proj₁ f , proj₂ f)) ≈ FMap MF (FMap (Monoidal.m-bi M) (proj₁ g , proj₂ g)) ] | |
158 ≈-cong {a} {b} {f} {g} f≈g = IsFunctor.≈-cong (isFunctor MF ) ( IsFunctor.≈-cong (isFunctor (Monoidal.m-bi M) ) f≈g ) | |
159 identity : {a : Obj (C × C)} → D [ FMap MF (FMap (Monoidal.m-bi M) (proj₁ (id1 (C × C) a) , proj₂ (id1 (C × C) a))) | |
160 ≈ id1 D (FObj MF (proj₁ a ⊗ proj₂ a)) ] | |
161 identity {a} = let open ≈-Reasoning D in begin | |
162 FMap MF (FMap (Monoidal.m-bi M) (proj₁ (id1 (C × C) a) , proj₂ (id1 (C × C) a))) | |
163 ≈⟨⟩ | |
164 FMap MF (FMap (Monoidal.m-bi M) (id1 (C × C) a ) ) | |
165 ≈⟨ fcong MF ( IsFunctor.identity (isFunctor (Monoidal.m-bi M) )) ⟩ | |
166 FMap MF (id1 C (proj₁ a ⊗ proj₂ a)) | |
167 ≈⟨ IsFunctor.identity (isFunctor MF) ⟩ | |
168 id1 D (FObj MF (proj₁ a ⊗ proj₂ a)) | |
169 ∎ | |
170 distr : {a b c : Obj (C × C)} {f : Hom (C × C) a b} {g : Hom (C × C) b c} → D [ | |
171 FMap MF (FMap (Monoidal.m-bi M) (proj₁ ((C × C) [ g o f ]) , proj₂ ((C × C) [ g o f ]))) | |
172 ≈ D [ FMap MF (FMap (Monoidal.m-bi M) (proj₁ g , proj₂ g)) o FMap MF (FMap (Monoidal.m-bi M) (proj₁ f , proj₂ f)) ] ] | |
173 distr {a} {b} {c} {f} {g} = let open ≈-Reasoning D in begin | |
174 FMap MF (FMap (Monoidal.m-bi M) (proj₁ ((C × C) [ g o f ]) , proj₂ ((C × C) [ g o f ]))) | |
175 ≈⟨⟩ | |
176 FMap MF (FMap (Monoidal.m-bi M) ( (C × C) [ g o f ] )) | |
177 ≈⟨ fcong MF ( IsFunctor.distr (isFunctor (Monoidal.m-bi M))) ⟩ | |
178 FMap MF (C [ FMap (Monoidal.m-bi M) g o FMap (Monoidal.m-bi M) f ]) | |
179 ≈⟨ IsFunctor.distr ( isFunctor MF ) ⟩ | |
180 FMap MF (FMap (Monoidal.m-bi M) (proj₁ g , proj₂ g)) o FMap MF (FMap (Monoidal.m-bi M) (proj₁ f , proj₂ f)) | |
181 ∎ | |
182 | |
696
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
183 |
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
184 record IsMonoidalFunctor {c₁ c₂ ℓ : Level} {C D : Category c₁ c₂ ℓ} ( M : Monoidal C ) ( N : Monoidal D ) |
698 | 185 ( MF : Functor C D ) |
702
d16327b48b83
Monoidal Functor ( two functor remains )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
701
diff
changeset
|
186 ( ψ : 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
|
187 : Set ( suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where |
698 | 188 _⊗_ : (x y : Obj C ) → Obj C |
700
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
189 _⊗_ 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
|
190 _□_ : {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
|
191 _□_ f g = FMap (Monoidal.m-bi M) ( f , g ) |
698 | 192 _●_ : (x y : Obj D ) → Obj D |
700
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
193 _●_ 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
|
194 _■_ : {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
|
195 _■_ 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
|
196 F● : Functor ( C × C ) D |
703 | 197 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
|
198 F⊗ : Functor ( C × C ) D |
703 | 199 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
|
200 field |
d16327b48b83
Monoidal Functor ( two functor remains )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
701
diff
changeset
|
201 φab : NTrans ( C × C ) D F● F⊗ |
698 | 202 open Iso |
203 open Monoidal | |
701
7a729bb62ce3
Monoidal Functor on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
700
diff
changeset
|
204 open IsMonoidal hiding ( _■_ ; _□_ ) |
699 | 205 αC : {a b c : Obj C} → Hom C (( a ⊗ b ) ⊗ c ) ( a ⊗ ( b ⊗ c ) ) |
206 αC {a} {b} {c} = ≅→ (mα-iso (isMonoidal M) {a} {b} {c}) | |
207 αD : {a b c : Obj D} → Hom D (( a ● b ) ● c ) ( a ● ( b ● c ) ) | |
208 α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
|
209 F : Obj C → Obj D |
7a729bb62ce3
Monoidal Functor on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
700
diff
changeset
|
210 F x = FObj MF x |
702
d16327b48b83
Monoidal Functor ( two functor remains )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
701
diff
changeset
|
211 φ : ( 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
|
212 φ 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
|
213 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
|
214 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
|
215 φ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
|
216 φ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
|
217 φ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
|
218 φ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
|
219 φ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
|
220 φ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
|
221 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
|
222 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
|
223 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
|
224 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
|
225 φ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
|
226 φ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
|
227 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
|
228 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
|
229 ρ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
|
230 ρ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
|
231 ψ●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
|
232 ψ●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
|
233 φ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
|
234 φ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
|
235 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
|
236 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
|
237 λ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
|
238 λ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
|
239 field |
700
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
240 comm1 : {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 ] ] ] |
702
d16327b48b83
Monoidal Functor ( two functor remains )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
701
diff
changeset
|
241 comm-idr : {a b : Obj C } → D [ D [ FρC {a} {b} o D [ φAIC {a} {b} o 1●ψ{a} {b} ] ] ≈ ρD {a} {b} ] |
d16327b48b83
Monoidal Functor ( two functor remains )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
701
diff
changeset
|
242 comm-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
|
243 |
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
244 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
|
245 : Set ( suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where |
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
246 _⊗_ : (x y : Obj C ) → Obj C |
700
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
247 _⊗_ x y = (IsMonoidal._□_ (Monoidal.isMonoidal M) ) x y |
696
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
248 _●_ : (x y : Obj D ) → Obj D |
700
cfd2d402c486
monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
699
diff
changeset
|
249 _●_ x y = (IsMonoidal._□_ (Monoidal.isMonoidal N) ) x y |
696
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
250 field |
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
251 MF : Functor C D |
702
d16327b48b83
Monoidal Functor ( two functor remains )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
701
diff
changeset
|
252 ψ : Hom D (Monoidal.m-i N) (FObj MF (Monoidal.m-i M) ) |
d16327b48b83
Monoidal Functor ( two functor remains )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
701
diff
changeset
|
253 isMonodailFunctor : IsMonoidalFunctor M N MF ψ |