Mercurial > hg > Members > kono > Proof > category

annotate monoidal.agda @ 706:dad072d52d0e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 22 Nov 2017 12:49:17 +0900
parents 73a998711118
children 808b03184fd3
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
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
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
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
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
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
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
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
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
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
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
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
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
65 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
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 ) ] ]
705
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
71 -- 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
72 α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
73 α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
74 α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
75 α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
76 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
77 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
78 α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
79 α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
80 α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
81 α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
82 α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
83 αAIB {a} {b} = ≅→ mα-iso
700
cfd2d402c486 monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 699
diff changeset
84 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
85 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
86 ρ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
87 ρ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
88
cfd2d402c486 monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 699
diff changeset
89 field
cfd2d402c486 monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 699
diff changeset
90 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
91 → 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
92 ≈ αA□BCD {a} {b} {c} {d} {e} ]
cfd2d402c486 monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 699
diff changeset
93 comm-unit : {a b : Obj C}
cfd2d402c486 monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 699
diff changeset
94 → 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
95
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
96 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
97 : Set ( suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
98 field
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
99 m-i : Obj C
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
100 m-bi : Functor ( C × C ) C
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
101 isMonoidal : IsMonoidal C m-i m-bi
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
102
705
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
103 ---------
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
104 --
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
105 -- Lax Monoidal Functor
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
106 --
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
107 -- N → M
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
108 --
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
109 ---------
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
110
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
111 ---------
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
112 --
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
113 -- 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
114 -- 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
115 --
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
116 -- F x ● F y
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
117 -- F ( x ⊗ y )
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
118 --
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
119 -- 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
120 --
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
121 -- φ : 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
122 --
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
123 -- 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
124 --
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
125 -- a given unit arrow
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
126 --
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
127 -- ψ : IN → IM
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
128
703
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
129 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
130 ( MF : Functor C D ) → Functor ( C × C ) D
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
131 Functor● C D N MF = record {
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
132 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
133 ; 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
134 ; isFunctor = record {
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
135 ≈-cong = ≈-cong
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
136 ; identity = identity
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
137 ; distr = distr
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
138 }
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
139 } where
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
140 _●_ : (x y : Obj D ) → Obj D
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
141 _●_ x y = (IsMonoidal._□_ (Monoidal.isMonoidal N) ) x y
704
b48c2d1c0796 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 703
diff changeset
142 _■_ : {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
143 _■_ f g = FMap (Monoidal.m-bi N) ( f , g )
b48c2d1c0796 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 703
diff changeset
144 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
145 F f = FMap MF f
703
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
146 ≈-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
147 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
148 ≈-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
149 F (proj₁ f) ■ F (proj₂ f)
703
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
150 ≈⟨ 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
151 F (proj₁ g) ■ F (proj₂ g)
703
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
152 ∎
704
b48c2d1c0796 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 703
diff changeset
153 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
154 ≈ 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
155 identity {a} = let open ≈-Reasoning D in begin
704
b48c2d1c0796 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 703
diff changeset
156 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
157 ≈⟨ 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
158 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
159 ≈⟨ IsFunctor.identity (isFunctor (Monoidal.m-bi N)) ⟩
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
160 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
161 ∎
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
162 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
163 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
164 ≈ 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
165 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
166 (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
167 ≈⟨ 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
168 ( 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
169 ≈⟨ IsFunctor.distr ( isFunctor (Monoidal.m-bi N)) ⟩
704
b48c2d1c0796 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 703
diff changeset
170 (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
171 ∎
696
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
172
703
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
173 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
174 ( MF : Functor C D ) → Functor ( C × C ) D
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
175 Functor⊗ C D M MF = record {
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
176 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
177 ; 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
178 ; isFunctor = record {
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
179 ≈-cong = ≈-cong
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
180 ; identity = identity
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
181 ; distr = distr
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
182 }
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
183 } where
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
184 _⊗_ : (x y : Obj C ) → Obj C
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
185 _⊗_ x y = (IsMonoidal._□_ (Monoidal.isMonoidal M) ) x y
704
b48c2d1c0796 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 703
diff changeset
186 _□_ : {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
187 _□_ f g = FMap (Monoidal.m-bi M) ( f , g )
b48c2d1c0796 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 703
diff changeset
188 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
189 F f = FMap MF f
703
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
190 ≈-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
191 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
192 ≈-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
193 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
194 ≈ id1 D (FObj MF (proj₁ a ⊗ proj₂ a)) ]
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
195 identity {a} = let open ≈-Reasoning D in begin
704
b48c2d1c0796 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 703
diff changeset
196 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
197 ≈⟨⟩
704
b48c2d1c0796 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 703
diff changeset
198 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
199 ≈⟨ 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
200 F (id1 C (proj₁ a ⊗ proj₂ a))
703
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
201 ≈⟨ IsFunctor.identity (isFunctor MF) ⟩
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
202 id1 D (FObj MF (proj₁ a ⊗ proj₂ a))
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
203 ∎
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
204 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
205 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
206 ≈ 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
207 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
208 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
209 ≈⟨⟩
704
b48c2d1c0796 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 703
diff changeset
210 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
211 ≈⟨ 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
212 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
213 ≈⟨ IsFunctor.distr ( isFunctor MF ) ⟩
704
b48c2d1c0796 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 703
diff changeset
214 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
215 ∎
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
216
696
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
217
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
218 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
219 ( MF : Functor C D )
702
d16327b48b83 Monoidal Functor ( two functor remains )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 701
diff changeset
220 ( ψ : 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
221 : Set ( suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where
698
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
222 _⊗_ : (x y : Obj C ) → Obj C
700
cfd2d402c486 monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 699
diff changeset
223 _⊗_ 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
224 _□_ : {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
225 _□_ 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
226 _●_ : (x y : Obj D ) → Obj D
700
cfd2d402c486 monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 699
diff changeset
227 _●_ 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
228 _■_ : {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
229 _■_ 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
230 F● : Functor ( C × C ) D
703
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
231 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
232 F⊗ : Functor ( C × C ) D
703
df3f1aae984f Monidal functor done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 702
diff changeset
233 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
234 field
d16327b48b83 Monoidal Functor ( two functor remains )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 701
diff changeset
235 φab : NTrans ( C × C ) D F● F⊗
698
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
236 open Iso
d648ebb8ac29 Monoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 697
diff changeset
237 open Monoidal
701
7a729bb62ce3 Monoidal Functor on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 700
diff changeset
238 open IsMonoidal hiding ( _■_ ; _□_ )
699
10ab28030c20 add definitions
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 698
diff changeset
239 α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
240 α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
241 α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
242 α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
243 F : Obj C → Obj D
7a729bb62ce3 Monoidal Functor on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 700
diff changeset
244 F x = FObj MF x
702
d16327b48b83 Monoidal Functor ( two functor remains )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 701
diff changeset
245 φ : ( 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
246 φ 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
247 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
248 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
249 φ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
250 φ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
251 φ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
252 φ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
253 φ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
254 φ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
255 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
256 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
257 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
258 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
259 φ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
260 φ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
261 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
262 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
263 ρ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
264 ρ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
265 ψ●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
266 ψ●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
267 φ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
268 φ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
269 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
270 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
271 λ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
272 λ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
273 field
705
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
274 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
275 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
276 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
277
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
278 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
279 : 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
280 field
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
281 MF : Functor C D
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
282 ψ : 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
283 isMonodailFunctor : IsMonoidalFunctor M N MF ψ
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
284
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
285 record MonoidalFunctorWithoutCommutativities {c₁ c₂ ℓ : Level} {C D : Category c₁ c₂ ℓ} ( M : Monoidal C ) ( N : Monoidal D )
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
286 : Set ( suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where
696
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
287 _⊗_ : (x y : Obj C ) → Obj C
700
cfd2d402c486 monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 699
diff changeset
288 _⊗_ 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
289 _●_ : (x y : Obj D ) → Obj D
700
cfd2d402c486 monodial cateogry and functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 699
diff changeset
290 _●_ 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
291 field
705
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
292 MF : Functor C D
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
293 unit : 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
294 ** : {a b : Obj C} → Hom D ((FObj MF a) ● (FObj MF b )) ( FObj MF ( a ⊗ b ) )
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
295
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
296 open import Category.Sets
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
297
706
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 705
diff changeset
298 import Relation.Binary.PropositionalEquality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 705
diff changeset
299 -- 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
300 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
301
705
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
302 data One {c : Level} : Set c where
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
303 OneObj : One -- () in Haskell ( or any one object set )
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
304
706
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 705
diff changeset
305 isoSets :{c₁ : Level} {a : Obj (Sets {c₁} ) } → Iso (Sets {c₁}) a ( a * One {c₁} )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 705
diff changeset
306 isoSets {a} = record {
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 705
diff changeset
307 ≅→ = λ x → ( x , OneObj ) ;
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 705
diff changeset
308 ≅← = λ x → proj₁ x ;
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 705
diff changeset
309 iso→ = refl ;
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 705
diff changeset
310 iso← = iso←
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 705
diff changeset
311 }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 705
diff changeset
312 where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 705
diff changeset
313 lemma : {a : Obj Sets } → (x : a * One) → (Sets [ (λ x₁ → x₁ , OneObj) o proj₁ ]) x ≡ id1 Sets (a * One) x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 705
diff changeset
314 lemma (_ , OneObj ) = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 705
diff changeset
315 iso← : {a : Obj Sets} → Sets [ Sets [ (λ x → x , OneObj) o proj₁ ] ≈ id1 Sets (a * One) ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 705
diff changeset
316 iso← {a} = extensionality Sets ( λ x → lemma x )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 705
diff changeset
317
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 705
diff changeset
318
705
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
319 record HaskellMonoidalFunctor {c₁ : Level} ( f : Functor (Sets {c₁}) (Sets {c₁}) )
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
320 : Set (suc (suc c₁)) where
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
321 field
706
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 705
diff changeset
322 unit : FObj f One
705
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
323 φ : {a b : Obj Sets} → Hom Sets ((FObj f a) * (FObj f b )) ( FObj f ( a * b ) )
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
324 ** : {a b : Obj Sets} → FObj f a → FObj f b → FObj f ( a * b )
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
325 ** x y = φ ( x , y )
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
326
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
327 -- HaskellMonoidalFunctor f → MonoidalFunctor
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
328
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
329 record Applicative {c₁ : Level} ( f : Functor (Sets {c₁}) (Sets {c₁}) )
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
330 : Set (suc (suc c₁)) where
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
331 field
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
332 pure : {a : Obj Sets} → Hom Sets a ( FObj f a )
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
333 <*> : {a b : Obj Sets} → FObj f ( a → b ) → FObj f a → FObj f b
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
334
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
335 lemma1 : {c₁ : Level} ( f : Functor (Sets {c₁}) (Sets {c₁}) ) → Applicative f → HaskellMonoidalFunctor f
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
336 lemma1 f app = record { unit = unit ; φ = φ }
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
337 where
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
338 open Applicative
706
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 705
diff changeset
339 unit : FObj f One
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 705
diff changeset
340 unit = pure app OneObj
705
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
341 φ : {a b : Obj Sets} → Hom Sets ((FObj f a) * (FObj f b )) ( FObj f ( a * b ) )
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
342 φ {a} {b} ( x , y ) = <*> app {!!} {!!}
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
343
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
344 lemma2 : {c₁ : Level} ( f : Functor (Sets {c₁}) (Sets {c₁}) ) → HaskellMonoidalFunctor f → Applicative f
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
345 lemma2 f app = record { pure = pure ; <*> = <*> }
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
346 where
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
347 open HaskellMonoidalFunctor
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
348 pure : {a : Obj Sets} → Hom Sets a ( FObj f a )
706
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 705
diff changeset
349 pure {a} x = {!!} -- (unit app)
705
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
350 <*> : {a b : Obj Sets} → FObj f ( a → b ) → FObj f a → FObj f b
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
351 <*> {a} {b} x = {!!}