Mercurial > hg > Members > kono > Proof > category
annotate monoidal.agda @ 698:d648ebb8ac29
Monoidal Functor
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 21 Nov 2017 09:57:42 +0900 |
parents | c68ba494abfd |
children | 10ab28030c20 |
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 |
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
27 infixr 9 _⊗_ |
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
28 _⊗_ : ( x y : Obj C ) → Obj C |
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
29 _⊗_ x y = FObj BI ( x , y ) |
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
30 field |
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
31 mα : {a b c : Obj C} → ( a ⊗ b) ⊗ c ≡ a ⊗ ( b ⊗ c ) |
698 | 32 mλ : (a : Obj C) → I ⊗ a ≡ a |
33 mσ : (a : Obj C) → a ⊗ I ≡ a | |
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 | |
47 infixr 9 _⊗_ | |
48 _⊗_ : ( x y : Obj C ) → Obj C | |
49 _⊗_ x y = FObj BI ( x , y ) | |
50 field | |
51 mα-iso : {a b c : Obj C} → Iso C ( ( a ⊗ b) ⊗ c) ( a ⊗ ( b ⊗ c ) ) | |
52 mλ-iso : {a : Obj C} → Iso C ( I ⊗ a) a | |
53 mσ-iso : {a : Obj C} → Iso C ( a ⊗ I) a | |
54 mα→nat1 : {a a' b c : Obj C} → ( f : Hom C a a' ) → | |
55 C [ C [ FMap BI ( f , id1 C ( b ⊗ c )) o ≅→ (mα-iso {a} {b} {c}) ] ≈ | |
56 C [ ≅→ (mα-iso ) o FMap BI ( FMap BI (f , id1 C b ) , id1 C c ) ] ] | |
57 mα→nat2 : {a b b' c : Obj C} → ( f : Hom C b b' ) → | |
58 C [ C [ FMap BI ( id1 C a , FMap BI ( f , id1 C c ) ) o ≅→ (mα-iso {a} {b} {c} ) ] ≈ | |
59 C [ ≅→ (mα-iso ) o FMap BI ( FMap BI (id1 C a , f ) , id1 C c ) ] ] | |
60 mα→nat3 : {a b c c' : Obj C} → ( f : Hom C c c' ) → | |
61 C [ C [ FMap BI ( id1 C a , FMap BI ( id1 C b , f ) ) o ≅→ (mα-iso {a} {b} {c} ) ] ≈ | |
62 C [ ≅→ (mα-iso ) o FMap BI ( id1 C ( a ⊗ b ) , f ) ] ] | |
63 mλ→nat : {a a' : Obj C} → ( f : Hom C a a' ) → | |
64 C [ C [ f o ≅→ (mλ-iso {a} ) ] ≈ | |
65 C [ ≅→ (mλ-iso ) o FMap BI ( id1 C I , f ) ] ] | |
66 mσ→nat : {a a' : Obj C} → ( f : Hom C a a' ) → | |
67 C [ C [ f o ≅→ (mσ-iso {a} ) ] ≈ | |
68 C [ ≅→ (mσ-iso ) o FMap BI ( f , id1 C I ) ] ] | |
696
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
69 |
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
70 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
|
71 : Set ( suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where |
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
72 field |
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
73 m-i : Obj C |
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
74 m-bi : Functor ( C × C ) C |
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
75 isMonoidal : IsMonoidal C m-i m-bi |
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 |
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
78 open import Category.Cat |
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
79 |
698 | 80 |
696
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
81 record IsMonoidalFunctor {c₁ c₂ ℓ : Level} {C D : Category c₁ c₂ ℓ} ( M : Monoidal C ) ( N : Monoidal D ) |
698 | 82 ( MF : Functor C D ) |
83 ( F● : Functor ( C × C ) D ) | |
84 ( F⊗ : Functor ( C × C ) D ) | |
85 ( φab : NTrans ( C × C ) D F● F⊗ ) | |
86 ( φ : 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
|
87 : Set ( suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where |
698 | 88 _⊗_ : (x y : Obj C ) → Obj C |
89 _⊗_ x y = (IsMonoidal._⊗_ (Monoidal.isMonoidal M) ) x y | |
90 _●_ : (x y : Obj D ) → Obj D | |
91 _●_ x y = (IsMonoidal._⊗_ (Monoidal.isMonoidal N) ) x y | |
92 open Iso | |
93 open Monoidal | |
94 open IsMonoidal hiding ( _⊗_ ) | |
95 αD : {a b c : Obj C} → Hom C (( a ⊗ b ) ⊗ c ) ( a ⊗ ( b ⊗ c ) ) | |
96 αD {a} {b} {c} = ≅→ (mα-iso (isMonoidal M) {a} {b} {c}) | |
696
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
97 field |
698 | 98 comm1 : {!!} |
696
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
99 |
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
100 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
|
101 : Set ( suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where |
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
102 _⊗_ : (x y : Obj C ) → Obj C |
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
103 _⊗_ x y = (IsMonoidal._⊗_ (Monoidal.isMonoidal M) ) x y |
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
104 _●_ : (x y : Obj D ) → Obj D |
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
105 _●_ x y = (IsMonoidal._⊗_ (Monoidal.isMonoidal N) ) x y |
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
106 field |
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
107 MF : Functor C D |
697 | 108 F● : Functor ( C × C ) D |
109 F● = record { | |
110 FObj = λ x → (FObj MF (proj₁ x) ) ● (FObj MF (proj₂ x) ) | |
111 ; FMap = λ {x : Obj ( C × C ) } {y} f → FMap (Monoidal.m-bi N) ( FMap MF (proj₁ f ) , FMap MF (proj₂ f) ) | |
696
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
112 ; isFunctor = record { |
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
113 } |
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
114 } |
697 | 115 F⊗ : Functor ( C × C ) D |
116 F⊗ = record { | |
117 FObj = λ x → FObj MF ( proj₁ x ⊗ proj₂ x ) | |
118 ; FMap = λ {a} {b} f → FMap MF ( FMap (Monoidal.m-bi M) ( proj₁ f , proj₂ f) ) | |
696
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
119 ; isFunctor = record { |
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
120 } |
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
121 } |
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
122 field |
697 | 123 φab : NTrans ( C × C ) D F● F⊗ |
696
10ccac3bc285
Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
124 φ : Hom D (Monoidal.m-i N) (FObj MF (Monoidal.m-i M) ) |
698 | 125 isMonodailFunctor : IsMonoidalFunctor M N MF F● F⊗ φab φ |