Mercurial > hg > Members > kono > Proof > category

annotate monoidal.agda @ 699:10ab28030c20

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add definitions
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 21 Nov 2017 10:28:53 +0900
parents d648ebb8ac29
children cfd2d402c486
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 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
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
16 record Iso {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ)
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
17 (x y : Obj C )
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
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
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
20 ≅→ : Hom C x y
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
21 ≅← : Hom C y x
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
22 iso→ : C [ C [ ≅← o ≅→ ] ≈ id1 C x ]
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
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
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
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
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
32 mλ : (a : Obj C) → I ⊗ a ≡ a
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
33 mσ : (a : Obj C) → a ⊗ I ≡ a
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
34
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
35 record StrictMonoidal {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ)
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
36 : Set ( suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
37 field
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
38 m-i : Obj C
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
39 m-bi : Functor ( C × C ) C
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
40 isMonoidal : IsStrictMonoidal C m-i m-bi
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
41
696
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42
698
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
43 -- non strict version includes 5 naturalities
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
44 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
45 : Set ( suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
46 open Iso
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
47 infixr 9 _⊗_
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
48 _⊗_ : ( x y : Obj C ) → Obj C
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
49 _⊗_ x y = FObj BI ( x , y )
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
50 field
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
51 mα-iso : {a b c : Obj C} → Iso C ( ( a ⊗ b) ⊗ c) ( a ⊗ ( b ⊗ c ) )
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
52 mλ-iso : {a : Obj C} → Iso C ( I ⊗ a) a
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
53 mσ-iso : {a : Obj C} → Iso C ( a ⊗ I) a
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
54 mα→nat1 : {a a' b c : Obj C} → ( f : Hom C a a' ) →
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
55 C [ C [ FMap BI ( f , id1 C ( b ⊗ c )) o ≅→ (mα-iso {a} {b} {c}) ] ≈
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
56 C [ ≅→ (mα-iso ) o FMap BI ( FMap BI (f , id1 C b ) , id1 C c ) ] ]
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
57 mα→nat2 : {a b b' c : Obj C} → ( f : Hom C b b' ) →
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
58 C [ C [ FMap BI ( id1 C a , FMap BI ( f , id1 C c ) ) o ≅→ (mα-iso {a} {b} {c} ) ] ≈
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
59 C [ ≅→ (mα-iso ) o FMap BI ( FMap BI (id1 C a , f ) , id1 C c ) ] ]
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
60 mα→nat3 : {a b c c' : Obj C} → ( f : Hom C c c' ) →
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
61 C [ C [ FMap BI ( id1 C a , FMap BI ( id1 C b , f ) ) o ≅→ (mα-iso {a} {b} {c} ) ] ≈
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
62 C [ ≅→ (mα-iso ) o FMap BI ( id1 C ( a ⊗ b ) , f ) ] ]
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
63 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
64 C [ C [ f o ≅→ (mλ-iso {a} ) ] ≈
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
65 C [ ≅→ (mλ-iso ) o FMap BI ( id1 C I , f ) ] ]
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
66 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
67 C [ C [ f o ≅→ (mσ-iso {a} ) ] ≈
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
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
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
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
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
82 ( MF : Functor C D )
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
83 ( F● : Functor ( C × C ) D )
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
84 ( F⊗ : Functor ( C × C ) D )
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
85 ( φab : NTrans ( C × C ) D F● F⊗ )
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
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
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
88 _⊗_ : (x y : Obj C ) → Obj C
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
89 _⊗_ x y = (IsMonoidal._⊗_ (Monoidal.isMonoidal M) ) x y
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
90 _●_ : (x y : Obj D ) → Obj D
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
91 _●_ x y = (IsMonoidal._⊗_ (Monoidal.isMonoidal N) ) x y
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
92 open Iso
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
93 open Monoidal
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
94 open IsMonoidal hiding ( _⊗_ )
699
10ab28030c20 add definitions
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 698
diff changeset
95 α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
96 α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
97 α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
98 αD {a} {b} {c} = ≅→ (mα-iso (isMonoidal N) {a} {b} {c})
10ab28030c20 add definitions
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 698
diff changeset
99 1●φBC : {a b c : Obj C} → Hom D ( FObj MF a ● ( FObj MF b ● FObj MF c ) ) ( FObj MF a ● ( FObj MF ( b ⊗ c ) ))
10ab28030c20 add definitions
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 698
diff changeset
100 1●φBC = {!!}
10ab28030c20 add definitions
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 698
diff changeset
101 φAB⊗C : {a b c : Obj C} → Hom D ( FObj MF a ● ( FObj MF ( b ⊗ c ) )) (FObj MF ( a ⊗ ( b ⊗ c )))
10ab28030c20 add definitions
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 698
diff changeset
102 φAB⊗C = {!!}
696
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
103 field
699
10ab28030c20 add definitions
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 698
diff changeset
104 comm1 : D [ D [ φAB⊗C o D [ 1●φBC o αD ] ] ≈ {!!} ]
696
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
105
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
106 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
107 : Set ( suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
108 _⊗_ : (x y : Obj C ) → Obj C
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
109 _⊗_ 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
110 _●_ : (x y : Obj D ) → Obj D
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
111 _●_ 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
112 field
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
113 MF : Functor C D
697
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 696
diff changeset
114 F● : Functor ( C × C ) D
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 696
diff changeset
115 F● = record {
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 696
diff changeset
116 FObj = λ x → (FObj MF (proj₁ x) ) ● (FObj MF (proj₂ x) )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 696
diff changeset
117 ; 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
118 ; isFunctor = record {
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
119 }
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
120 }
697
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 696
diff changeset
121 F⊗ : Functor ( C × C ) D
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 696
diff changeset
122 F⊗ = record {
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 696
diff changeset
123 FObj = λ x → FObj MF ( proj₁ x ⊗ proj₂ x )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 696
diff changeset
124 ; 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
125 ; isFunctor = record {
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
126 }
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
127 }
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
128 field
697
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 696
diff changeset
129 φ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
130 φ : Hom D (Monoidal.m-i N) (FObj MF (Monoidal.m-i M) )
698
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
131 isMonodailFunctor : IsMonoidalFunctor M N MF F● F⊗ φab φ