Mercurial > hg > Members > kono > Proof > category

comparison monoidal.agda @ 702:d16327b48b83

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Monoidal Functor ( two functor remains )
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 22 Nov 2017 02:55:36 +0900
parents 7a729bb62ce3
children df3f1aae984f
comparison
equal deleted inserted replaced
701:7a729bb62ce3 702:d16327b48b83
100 isMonoidal : IsMonoidal C m-i m-bi 100 isMonoidal : IsMonoidal C m-i m-bi
101 101
102 102
103 open import Category.Cat 103 open import Category.Cat
104 104
105
106 record IsMonoidalFunctor {c₁ c₂ ℓ : Level} {C D : Category c₁ c₂ ℓ} ( M : Monoidal C ) ( N : Monoidal D ) 105 record IsMonoidalFunctor {c₁ c₂ ℓ : Level} {C D : Category c₁ c₂ ℓ} ( M : Monoidal C ) ( N : Monoidal D )
107 ( MF : Functor C D ) 106 ( MF : Functor C D )
108 ( F● : Functor ( C × C ) D ) 107 ( ψ : Hom D (Monoidal.m-i N) (FObj MF (Monoidal.m-i M) ) )
109 ( F⊗ : Functor ( C × C ) D )
110 ( φab : NTrans ( C × C ) D F● F⊗ )
111 ( φ : Hom D (Monoidal.m-i N) (FObj MF (Monoidal.m-i M) ) )
112 : Set ( suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where 108 : Set ( suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where
113 _⊗_ : (x y : Obj C ) → Obj C 109 _⊗_ : (x y : Obj C ) → Obj C
114 _⊗_ x y = (IsMonoidal._□_ (Monoidal.isMonoidal M) ) x y 110 _⊗_ x y = (IsMonoidal._□_ (Monoidal.isMonoidal M) ) x y
115 _□_ : {a b c d : Obj C } ( f : Hom C a c ) ( g : Hom C b d ) → Hom C ( a ⊗ b ) ( c ⊗ d ) 111 _□_ : {a b c d : Obj C } ( f : Hom C a c ) ( g : Hom C b d ) → Hom C ( a ⊗ b ) ( c ⊗ d )
116 _□_ f g = FMap (Monoidal.m-bi M) ( f , g ) 112 _□_ f g = FMap (Monoidal.m-bi M) ( f , g )
117 _●_ : (x y : Obj D ) → Obj D 113 _●_ : (x y : Obj D ) → Obj D
118 _●_ x y = (IsMonoidal._□_ (Monoidal.isMonoidal N) ) x y 114 _●_ x y = (IsMonoidal._□_ (Monoidal.isMonoidal N) ) x y
119 _■_ : {a b c d : Obj D } ( f : Hom D a c ) ( g : Hom D b d ) → Hom D ( a ● b ) ( c ● d ) 115 _■_ : {a b c d : Obj D } ( f : Hom D a c ) ( g : Hom D b d ) → Hom D ( a ● b ) ( c ● d )
120 _■_ f g = FMap (Monoidal.m-bi N) ( f , g ) 116 _■_ f g = FMap (Monoidal.m-bi N) ( f , g )
117 F● : Functor ( C × C ) D
118 F● = record {
119 FObj = λ x → (FObj MF (proj₁ x) ) ● (FObj MF (proj₂ x) )
120 ; FMap = λ {x : Obj ( C × C ) } {y} f → FMap (Monoidal.m-bi N) ( FMap MF (proj₁ f ) , FMap MF (proj₂ f) )
121 ; isFunctor = record {
122 ≈-cong = {!!}
123 ; identity = {!!}
124 ; distr = {!!}
125 }
126 }
127 F⊗ : Functor ( C × C ) D
128 F⊗ = record {
129 FObj = λ x → FObj MF ( proj₁ x ⊗ proj₂ x )
130 ; FMap = λ {a} {b} f → FMap MF ( FMap (Monoidal.m-bi M) ( proj₁ f , proj₂ f) )
131 ; isFunctor = record {
132 ≈-cong = {!!}
133 ; identity = {!!}
134 ; distr = {!!}
135 }
136 }
137 field
138 φab : NTrans ( C × C ) D F● F⊗
121 open Iso 139 open Iso
122 open Monoidal 140 open Monoidal
123 open IsMonoidal hiding ( _■_ ; _□_ ) 141 open IsMonoidal hiding ( _■_ ; _□_ )
124 αC : {a b c : Obj C} → Hom C (( a ⊗ b ) ⊗ c ) ( a ⊗ ( b ⊗ c ) ) 142 αC : {a b c : Obj C} → Hom C (( a ⊗ b ) ⊗ c ) ( a ⊗ ( b ⊗ c ) )
125 αC {a} {b} {c} = ≅→ (mα-iso (isMonoidal M) {a} {b} {c}) 143 αC {a} {b} {c} = ≅→ (mα-iso (isMonoidal M) {a} {b} {c})
126 αD : {a b c : Obj D} → Hom D (( a ● b ) ● c ) ( a ● ( b ● c ) ) 144 αD : {a b c : Obj D} → Hom D (( a ● b ) ● c ) ( a ● ( b ● c ) )
127 αD {a} {b} {c} = ≅→ (mα-iso (isMonoidal N) {a} {b} {c}) 145 αD {a} {b} {c} = ≅→ (mα-iso (isMonoidal N) {a} {b} {c})
128 F : Obj C → Obj D 146 F : Obj C → Obj D
129 F x = FObj MF x 147 F x = FObj MF x
148 φ : ( x y : Obj C ) → Hom D ( FObj F● (x , y) ) ( FObj F⊗ ( x , y ))
149 φ x y = NTrans.TMap φab ( x , y )
130 1●φBC : {a b c : Obj C} → Hom D ( F a ● ( F b ● F c ) ) ( F a ● ( F ( b ⊗ c ) )) 150 1●φBC : {a b c : Obj C} → Hom D ( F a ● ( F b ● F c ) ) ( F a ● ( F ( b ⊗ c ) ))
131 1●φBC {a} {b} {c} = id1 D (F a) ■ {!!} 151 1●φBC {a} {b} {c} = id1 D (F a) ■ φ b c
132 φAB⊗C : {a b c : Obj C} → Hom D ( F a ● ( F ( b ⊗ c ) )) (F ( a ⊗ ( b ⊗ c ))) 152 φAB⊗C : {a b c : Obj C} → Hom D ( F a ● ( F ( b ⊗ c ) )) (F ( a ⊗ ( b ⊗ c )))
133 φAB⊗C {a} {b} {c} = {!!} 153 φAB⊗C {a} {b} {c} = φ a (b ⊗ c )
134 φAB●1 : {a b c : Obj C} → Hom D ( ( F a ● F b ) ● F c ) ( F ( a ⊗ b ) ● F c ) 154 φAB●1 : {a b c : Obj C} → Hom D ( ( F a ● F b ) ● F c ) ( F ( a ⊗ b ) ● F c )
135 φAB●1 {a} {b} {c} = {!!} ■ id1 D (F c) 155 φAB●1 {a} {b} {c} = φ a b ■ id1 D (F c)
136 φA⊗BC : {a b c : Obj C} → Hom D ( F ( a ⊗ b ) ● F c ) (F ( (a ⊗ b ) ⊗ c )) 156 φA⊗BC : {a b c : Obj C} → Hom D ( F ( a ⊗ b ) ● F c ) (F ( (a ⊗ b ) ⊗ c ))
137 φA⊗BC {a} {b} {c} = {!!} 157 φA⊗BC {a} {b} {c} = φ ( a ⊗ b ) c
138 FαC : {a b c : Obj C} → Hom D (F ( (a ⊗ b ) ⊗ c )) (F ( a ⊗ ( b ⊗ c ))) 158 FαC : {a b c : Obj C} → Hom D (F ( (a ⊗ b ) ⊗ c )) (F ( a ⊗ ( b ⊗ c )))
139 FαC {a} {b} {c} = FMap MF ( ≅→ (mα-iso (isMonoidal M) {a} {b} {c}) ) 159 FαC {a} {b} {c} = FMap MF ( ≅→ (mα-iso (isMonoidal M) {a} {b} {c}) )
140 1●φ : { a b : Obj C } → Hom D (F a ● Monoidal.m-i N ) ( F a ● F ( Monoidal.m-i M ) ) 160 1●ψ : { a b : Obj C } → Hom D (F a ● Monoidal.m-i N ) ( F a ● F ( Monoidal.m-i M ) )
141 1●φ {a} {b} = id1 D (F a) ■ φ 161 1●ψ{a} {b} = id1 D (F a) ■ ψ
142 φAIC : { a b : Obj C } → Hom D ( F a ● F ( Monoidal.m-i M ) ) (F ( a ⊗ Monoidal.m-i M )) 162 φAIC : { a b : Obj C } → Hom D ( F a ● F ( Monoidal.m-i M ) ) (F ( a ⊗ Monoidal.m-i M ))
143 φAIC {a} {b} = {!!} 163 φAIC {a} {b} = φ a ( Monoidal.m-i M )
144 FρC : { a b : Obj C } → Hom D (F ( a ⊗ Monoidal.m-i M ))( F a ) 164 FρC : { a b : Obj C } → Hom D (F ( a ⊗ Monoidal.m-i M ))( F a )
145 FρC {a} {b} = FMap MF ( ≅→ (mρ-iso (isMonoidal M) {a} ) ) 165 FρC {a} {b} = FMap MF ( ≅→ (mρ-iso (isMonoidal M) {a} ) )
146 ρD : { a b : Obj C } → Hom D (F a ● Monoidal.m-i N ) ( F a ) 166 ρD : { a b : Obj C } → Hom D (F a ● Monoidal.m-i N ) ( F a )
147 ρD {a} {b} = ≅→ (mρ-iso (isMonoidal N) {F a} ) 167 ρD {a} {b} = ≅→ (mρ-iso (isMonoidal N) {F a} )
148 φ●1 : { a b : Obj C } → Hom D (Monoidal.m-i N ● F b ) ( F ( Monoidal.m-i M ) ● F b ) 168 ψ●1 : { a b : Obj C } → Hom D (Monoidal.m-i N ● F b ) ( F ( Monoidal.m-i M ) ● F b )
149 φ●1 {a} {b} = φ ■ id1 D (F b) 169 ψ●1 {a} {b} = ψ ■ id1 D (F b)
150 φICB : { a b : Obj C } → Hom D ( F ( Monoidal.m-i M ) ● F b ) ( F ( ( Monoidal.m-i M ) ⊗ b ) ) 170 φICB : { a b : Obj C } → Hom D ( F ( Monoidal.m-i M ) ● F b ) ( F ( ( Monoidal.m-i M ) ⊗ b ) )
151 φICB {a} {b} = {!!} 171 φICB {a} {b} = φ ( Monoidal.m-i M ) b
152 FλD : { a b : Obj C } → Hom D ( F ( ( Monoidal.m-i M ) ⊗ b ) ) (F b ) 172 FλD : { a b : Obj C } → Hom D ( F ( ( Monoidal.m-i M ) ⊗ b ) ) (F b )
153 FλD {a} {b} = FMap MF ( ≅→ (mλ-iso (isMonoidal M) {b} ) ) 173 FλD {a} {b} = FMap MF ( ≅→ (mλ-iso (isMonoidal M) {b} ) )
154 λD : { a b : Obj C } → Hom D (Monoidal.m-i N ● F b ) (F b ) 174 λD : { a b : Obj C } → Hom D (Monoidal.m-i N ● F b ) (F b )
155 λD {a} {b} = ≅→ (mλ-iso (isMonoidal N) {F b} ) 175 λD {a} {b} = ≅→ (mλ-iso (isMonoidal N) {F b} )
156 field 176 field
157 comm1 : {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 ] ] ] 177 comm1 : {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 ] ] ]
158 comm-idr : {a b : Obj C } → D [ D [ FρC {a} {b} o D [ φAIC {a} {b} o 1●φ {a} {b} ] ] ≈ ρD {a} {b} ] 178 comm-idr : {a b : Obj C } → D [ D [ FρC {a} {b} o D [ φAIC {a} {b} o 1●ψ{a} {b} ] ] ≈ ρD {a} {b} ]
159 comm-idl : {a b : Obj C } → D [ D [ FλD {a} {b} o D [ φICB {a} {b} o φ●1 {a} {b} ] ] ≈ λD {a} {b} ] 179 comm-idl : {a b : Obj C } → D [ D [ FλD {a} {b} o D [ φICB {a} {b} o ψ●1 {a} {b} ] ] ≈ λD {a} {b} ]
180 where
160 181
161 record MonoidalFunctor {c₁ c₂ ℓ : Level} {C D : Category c₁ c₂ ℓ} ( M : Monoidal C ) ( N : Monoidal D ) 182 record MonoidalFunctor {c₁ c₂ ℓ : Level} {C D : Category c₁ c₂ ℓ} ( M : Monoidal C ) ( N : Monoidal D )
162 : Set ( suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where 183 : Set ( suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where
163 _⊗_ : (x y : Obj C ) → Obj C 184 _⊗_ : (x y : Obj C ) → Obj C
164 _⊗_ x y = (IsMonoidal._□_ (Monoidal.isMonoidal M) ) x y 185 _⊗_ x y = (IsMonoidal._□_ (Monoidal.isMonoidal M) ) x y
165 _●_ : (x y : Obj D ) → Obj D 186 _●_ : (x y : Obj D ) → Obj D
166 _●_ x y = (IsMonoidal._□_ (Monoidal.isMonoidal N) ) x y 187 _●_ x y = (IsMonoidal._□_ (Monoidal.isMonoidal N) ) x y
167 field 188 field
168 MF : Functor C D 189 MF : Functor C D
169 F● : Functor ( C × C ) D 190 ψ : Hom D (Monoidal.m-i N) (FObj MF (Monoidal.m-i M) )
170 F● = record { 191 isMonodailFunctor : IsMonoidalFunctor M N MF ψ
171 FObj = λ x → (FObj MF (proj₁ x) ) ● (FObj MF (proj₂ x) )
172 ; FMap = λ {x : Obj ( C × C ) } {y} f → FMap (Monoidal.m-bi N) ( FMap MF (proj₁ f ) , FMap MF (proj₂ f) )
173 ; isFunctor = record {
174 }
175 }
176 F⊗ : Functor ( C × C ) D
177 F⊗ = record {
178 FObj = λ x → FObj MF ( proj₁ x ⊗ proj₂ x )
179 ; FMap = λ {a} {b} f → FMap MF ( FMap (Monoidal.m-bi M) ( proj₁ f , proj₂ f) )
180 ; isFunctor = record {
181 }
182 }
183 field
184 φab : NTrans ( C × C ) D F● F⊗
185 φ : Hom D (Monoidal.m-i N) (FObj MF (Monoidal.m-i M) )
186 isMonodailFunctor : IsMonoidalFunctor M N MF F● F⊗ φab φ