Mercurial > hg > Members > kono > Proof > category

comparison 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
comparison
equal deleted inserted replaced
695:7a6ee564e3a8 696:10ccac3bc285
1 open import Level
2 open import Level
3 open import Level
4 open import Category
5 module monoidal where
6
7 open import Data.Product renaming (_×_ to _*_)
8 open import Category.Constructions.Product
9 open import HomReasoning
10 open import cat-utility
11 open import Relation.Binary.Core
12 open import Relation.Binary
13
14 open Functor
15
16 record _≅_ {ℓ : Level } ( C B : Set ℓ ) : Set (suc ℓ ) where
17 field
18 ≅→ : C → B
19 ≅← : B → C
20 ≅Id→ : {x : C} → ≅← ( ≅→ x ) ≡ x
21 ≅Id← : {x : B} → ≅→ ( ≅← x ) ≡ x
22
23 infix 4 _≅_
24
25 record IsMonoidal {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ) (I : Obj C) ( BI : Functor ( C × C ) C )
26 : Set ( suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where
27 infixr 9 _⊗_
28 _⊗_ : ( x y : Obj C ) → Obj C
29 _⊗_ x y = FObj BI ( x , y )
30 field
31 mα : {a b c : Obj C} → ( a ⊗ b) ⊗ c ≡ a ⊗ ( b ⊗ c )
32 mλa : (a : Obj C) → I ⊗ a ≡ a
33 mσa : (a : Obj C) → a ⊗ I ≡ a
34
35 -- -- non strict version includes 6 naturalities
36 -- mα→ : {a b c : Obj C} → Hom C ( ( a ⊗ b) ⊗ c) ( a ⊗ ( b ⊗ c ) )
37 -- mα← : {a b c : Obj C} → Hom C ( a ⊗ ( b ⊗ c )) ( ( a ⊗ b) ⊗ c)
38 -- mα-iso→ : {a b c : Obj C} → C [ C [ mα← o mα→ ] ≈ id1 C (( a ⊗ b) ⊗ c ) ]
39 -- mα-iso← : {a b c : Obj C} → C [ C [ mα→ o mα← ] ≈ id1 C ( a ⊗ (b ⊗ c )) ]
40 -- mα→nat1 : {a a' b c : Obj C} → ( f : Hom C a a' ) →
41 -- C [ C [ FMap BI ( f , id1 C (FObj BI ( b , c ) )) o mα→ {a} ] ≈
42 -- C [ mα→ {a'} o FMap BI ( FMap BI (f , id1 C b ) , id1 C c ) ] ]
43
44 record Monoidal {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ)
45 : Set ( suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where
46 field
47 m-i : Obj C
48 m-bi : Functor ( C × C ) C
49 isMonoidal : IsMonoidal C m-i m-bi
50
51
52 open import Category.Cat
53
54 record IsMonoidalFunctor {c₁ c₂ ℓ : Level} {C D : Category c₁ c₂ ℓ} ( M : Monoidal C ) ( N : Monoidal D )
55 : Set ( suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where
56 field
57 a : {!!}
58
59 record MonoidalFunctor {c₁ c₂ ℓ : Level} {C D : Category c₁ c₂ ℓ} ( M : Monoidal C ) ( N : Monoidal D )
60 : Set ( suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where
61 _⊗_ : (x y : Obj C ) → Obj C
62 _⊗_ x y = (IsMonoidal._⊗_ (Monoidal.isMonoidal M) ) x y
63 _●_ : (x y : Obj D ) → Obj D
64 _●_ x y = (IsMonoidal._⊗_ (Monoidal.isMonoidal N) ) x y
65 field
66 MF : Functor C D
67 F● : (a b : Obj C ) → Functor ( C × C ) D
68 F● a b = record {
69 FObj = λ x → (FObj MF a) ● (FObj MF b)
70 ; FMap = λ {a} {b} f → FMap (Monoidal.m-bi N) ( FMap MF ? , FMap MF {!!} )
71 ; isFunctor = record {
72 }
73 }
74 F⊗ : (a b : Obj C ) → Functor ( C × C ) D
75 F⊗ a b = record {
76 FObj = λ x → FObj MF ( a ⊗ b )
77 ; FMap = λ {a} {b} f → FMap MF ( FMap (Monoidal.m-bi M) ( {!!} , {!!} ) )
78 ; isFunctor = record {
79 }
80 }
81 field
82 φab : {a b : Obj C} → NTrans ( C × C ) D (F● a b) (F⊗ a b )
83 φ : Hom D (Monoidal.m-i N) (FObj MF (Monoidal.m-i M) )
84 isMonodailFunctor : IsMonoidalFunctor M N