Mercurial > hg > Members > kono > Proof > category

annotate monoidal.agda @ 696:10ccac3bc285

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Monoidal category and applicative functor
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 20 Nov 2017 22:52:55 +0900
parents
children c68ba494abfd
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
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 record _≅_ {ℓ : Level } ( C B : Set ℓ ) : Set (suc ℓ ) where
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 field
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 ≅→ : C → B
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 ≅← : B → C
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 ≅Id→ : {x : C} → ≅← ( ≅→ x ) ≡ x
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 ≅Id← : {x : B} → ≅→ ( ≅← x ) ≡ x
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 infix 4 _≅_
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 record IsMonoidal {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ) (I : Obj C) ( BI : Functor ( C × C ) C )
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 )
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 mλa : (a : Obj C) → I ⊗ a ≡ a
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33 mσa : (a : Obj C) → a ⊗ I ≡ a
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 -- -- non strict version includes 6 naturalities
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36 -- mα→ : {a b c : Obj C} → Hom C ( ( a ⊗ b) ⊗ c) ( a ⊗ ( b ⊗ c ) )
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 -- mα← : {a b c : Obj C} → Hom C ( a ⊗ ( b ⊗ c )) ( ( a ⊗ b) ⊗ c)
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 -- mα-iso→ : {a b c : Obj C} → C [ C [ mα← o mα→ ] ≈ id1 C (( a ⊗ b) ⊗ c ) ]
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39 -- mα-iso← : {a b c : Obj C} → C [ C [ mα→ o mα← ] ≈ id1 C ( a ⊗ (b ⊗ c )) ]
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40 -- mα→nat1 : {a a' b c : Obj C} → ( f : Hom C a a' ) →
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41 -- C [ C [ FMap BI ( f , id1 C (FObj BI ( b , c ) )) o mα→ {a} ] ≈
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 -- C [ mα→ {a'} o FMap BI ( FMap BI (f , id1 C b ) , id1 C c ) ] ]
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44 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
45 : Set ( suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46 field
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
47 m-i : Obj C
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
48 m-bi : Functor ( C × C ) C
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
49 isMonoidal : IsMonoidal C m-i m-bi
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
50
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
51
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
52 open import Category.Cat
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
53
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
54 record IsMonoidalFunctor {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
55 : Set ( suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
56 field
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
57 a : {!!}
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
58
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
59 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
60 : Set ( suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
61 _⊗_ : (x y : Obj C ) → Obj C
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
62 _⊗_ 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
63 _●_ : (x y : Obj D ) → Obj D
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
64 _●_ 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
65 field
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
66 MF : Functor C D
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
67 F● : (a b : Obj C ) → Functor ( C × C ) D
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
68 F● a b = record {
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
69 FObj = λ x → (FObj MF a) ● (FObj MF b)
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
70 ; FMap = λ {a} {b} f → FMap (Monoidal.m-bi N) ( FMap MF ? , FMap MF {!!} )
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
71 ; isFunctor = record {
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
72 }
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
73 }
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
74 F⊗ : (a b : Obj C ) → Functor ( C × C ) D
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
75 F⊗ a b = record {
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
76 FObj = λ x → FObj MF ( a ⊗ b )
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
77 ; FMap = λ {a} {b} f → FMap MF ( FMap (Monoidal.m-bi M) ( {!!} , {!!} ) )
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
78 ; isFunctor = record {
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
79 }
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
80 }
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
81 field
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
82 φab : {a b : Obj C} → NTrans ( C × C ) D (F● a b) (F⊗ a b )
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
83 φ : Hom D (Monoidal.m-i N) (FObj MF (Monoidal.m-i M) )
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
84 isMonodailFunctor : IsMonoidalFunctor M N