Mercurial > hg > Members > kono > Proof > category

comparison monoidal.agda @ 701:7a729bb62ce3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Monoidal Functor on going ...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 22 Nov 2017 02:09:22 +0900
parents cfd2d402c486
children d16327b48b83
comparison
equal deleted inserted replaced
700:cfd2d402c486 701:7a729bb62ce3
67 C [ ≅→ (mλ-iso ) o ( id1 C I ■ f ) ] ] 67 C [ ≅→ (mλ-iso ) o ( id1 C I ■ f ) ] ]
68 mρ→nat : {a a' : Obj C} → ( f : Hom C a a' ) → 68 mρ→nat : {a a' : Obj C} → ( f : Hom C a a' ) →
69 C [ C [ f o ≅→ (mρ-iso {a} ) ] ≈ 69 C [ C [ f o ≅→ (mρ-iso {a} ) ] ≈
70 C [ ≅→ (mρ-iso ) o ( f ■ id1 C I ) ] ] 70 C [ ≅→ (mρ-iso ) o ( f ■ id1 C I ) ] ]
71 αABC□1D : {a b c d e : Obj C } → Hom C (((a □ b) □ c ) □ d) ((a □ (b □ c)) □ d) 71 αABC□1D : {a b c d e : Obj C } → Hom C (((a □ b) □ c ) □ d) ((a □ (b □ c)) □ d)
72 αABC□1D = {!!} 72 αABC□1D {a} {b} {c} {d} {e} = ( ≅→ mα-iso ■ id1 C d )
73 αAB□CD : {a b c d e : Obj C } → Hom C ((a □ (b □ c)) □ d) (a □ ((b □ c ) □ d)) 73 αAB□CD : {a b c d e : Obj C } → Hom C ((a □ (b □ c)) □ d) (a □ ((b □ c ) □ d))
74 αAB□CD = {!!} 74 αAB□CD {a} {b} {c} {d} {e} = ≅→ mα-iso
75 1A□BCD : {a b c d e : Obj C } → Hom C (a □ ((b □ c ) □ d)) (a □ (b □ ( c □ d) )) 75 1A□BCD : {a b c d e : Obj C } → Hom C (a □ ((b □ c ) □ d)) (a □ (b □ ( c □ d) ))
76 1A□BCD = {!!} 76 1A□BCD {a} {b} {c} {d} {e} = ( id1 C a ■ ≅→ mα-iso )
77 αABC□D : {a b c d e : Obj C } → Hom C (a □ (b □ ( c □ d) )) ((a □ b ) □ (c □ d)) 77 αABC□D : {a b c d e : Obj C } → Hom C (a □ (b □ ( c □ d) )) ((a □ b ) □ (c □ d))
78 αABC□D = {!!} 78 αABC□D {a} {b} {c} {d} {e} = ≅← mα-iso
79 αA□BCD : {a b c d e : Obj C } → Hom C (((a □ b) □ c ) □ d) ((a □ b ) □ (c □ d)) 79 αA□BCD : {a b c d e : Obj C } → Hom C (((a □ b) □ c ) □ d) ((a □ b ) □ (c □ d))
80 αA□BCD = {!!} 80 αA□BCD {a} {b} {c} {d} {e} = ≅→ mα-iso
81 αAIB : {a b : Obj C } → Hom C (( a □ I ) □ b ) (a □ ( I □ b )) 81 αAIB : {a b : Obj C } → Hom C (( a □ I ) □ b ) (a □ ( I □ b ))
82 αAIB = {!!} 82 αAIB {a} {b} = ≅→ mα-iso
83 1A□λB : {a b : Obj C } → Hom C (a □ ( I □ b )) ( a □ b ) 83 1A□λB : {a b : Obj C } → Hom C (a □ ( I □ b )) ( a □ b )
84 1A□λB = {!!} 84 1A□λB {a} {b} = id1 C a ■ ≅→ mλ-iso
85 ρA□IB : {a b : Obj C } → Hom C (( a □ I ) □ b ) ( a □ b ) 85 ρA□IB : {a b : Obj C } → Hom C (( a □ I ) □ b ) ( a □ b )
86 ρA□IB = {!!} 86 ρA□IB {a} {b} = ≅→ mρ-iso ■ id1 C b
87 87
88 field 88 field
89 comm-penta : {a b c d e : Obj C} 89 comm-penta : {a b c d e : Obj C}
90 → 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} ] ] ] 90 → 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} ] ] ]
91 ≈ αA□BCD {a} {b} {c} {d} {e} ] 91 ≈ αA□BCD {a} {b} {c} {d} {e} ]
118 _●_ x y = (IsMonoidal._□_ (Monoidal.isMonoidal N) ) x y 118 _●_ 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 ) 119 _■_ : {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 ) 120 _■_ f g = FMap (Monoidal.m-bi N) ( f , g )
121 open Iso 121 open Iso
122 open Monoidal 122 open Monoidal
123 open IsMonoidal 123 open IsMonoidal hiding ( _■_ ; _□_ )
124 αC : {a b c : Obj C} → Hom C (( a ⊗ b ) ⊗ c ) ( a ⊗ ( b ⊗ c ) ) 124 α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}) 125 α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 ) ) 126 α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}) 127 αD {a} {b} {c} = ≅→ (mα-iso (isMonoidal N) {a} {b} {c})
128 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 ) )) 128 F : Obj C → Obj D
129 1●φBC = {!!} 129 F x = FObj MF x
130 φAB⊗C : {a b c : Obj C} → Hom D ( FObj MF a ● ( FObj MF ( b ⊗ c ) )) (FObj MF ( a ⊗ ( b ⊗ c ))) 130 1●φBC : {a b c : Obj C} → Hom D ( F a ● ( F b ● F c ) ) ( F a ● ( F ( b ⊗ c ) ))
131 φAB⊗C = {!!} 131 1●φBC {a} {b} {c} = id1 D (F a) ■ {!!}
132 φAB●1 : {a b c : Obj C} → Hom D ( ( FObj MF a ● FObj MF b ) ● FObj MF c ) ( FObj MF ( a ⊗ b ) ● FObj MF c ) 132 φAB⊗C : {a b c : Obj C} → Hom D ( F a ● ( F ( b ⊗ c ) )) (F ( a ⊗ ( b ⊗ c )))
133 φAB●1 = {!!} 133 φAB⊗C {a} {b} {c} = {!!}
134 φA⊗BC : {a b c : Obj C} → Hom D ( FObj MF ( a ⊗ b ) ● FObj MF c ) (FObj MF ( (a ⊗ b ) ⊗ c )) 134 φAB●1 : {a b c : Obj C} → Hom D ( ( F a ● F b ) ● F c ) ( F ( a ⊗ b ) ● F c )
135 φA⊗BC = {!!} 135 φAB●1 {a} {b} {c} = {!!} ■ id1 D (F c)
136 FαC : {a b c : Obj C} → Hom D (FObj MF ( (a ⊗ b ) ⊗ c )) (FObj MF ( a ⊗ ( b ⊗ c ))) 136 φA⊗BC : {a b c : Obj C} → Hom D ( F ( a ⊗ b ) ● F c ) (F ( (a ⊗ b ) ⊗ c ))
137 FαC = {!!} 137 φA⊗BC {a} {b} {c} = {!!}
138 1●φ : { a b : Obj C } → Hom D (FObj MF a ● Monoidal.m-i N ) ( FObj MF a ● FObj MF ( Monoidal.m-i M ) ) 138 FαC : {a b c : Obj C} → Hom D (F ( (a ⊗ b ) ⊗ c )) (F ( a ⊗ ( b ⊗ c )))
139 1●φ = {!!} 139 FαC {a} {b} {c} = FMap MF ( ≅→ (mα-iso (isMonoidal M) {a} {b} {c}) )
140 φAIC : { a b : Obj C } → Hom D ( FObj MF a ● FObj MF ( Monoidal.m-i M ) ) (FObj MF ( a ⊗ Monoidal.m-i M )) 140 1●φ : { a b : Obj C } → Hom D (F a ● Monoidal.m-i N ) ( F a ● F ( Monoidal.m-i M ) )
141 φAIC = {!!} 141 1●φ {a} {b} = id1 D (F a) ■ φ
142 FρC : { a b : Obj C } → Hom D (FObj MF ( a ⊗ Monoidal.m-i M ))( FObj MF a ) 142 φAIC : { a b : Obj C } → Hom D ( F a ● F ( Monoidal.m-i M ) ) (F ( a ⊗ Monoidal.m-i M ))
143 FρC = {!!} 143 φAIC {a} {b} = {!!}
144 ρD : { a b : Obj C } → Hom D (FObj MF a ● Monoidal.m-i N ) ( FObj MF a ) 144 FρC : { a b : Obj C } → Hom D (F ( a ⊗ Monoidal.m-i M ))( F a )
145 ρD = {!!} 145 FρC {a} {b} = FMap MF ( ≅→ (mρ-iso (isMonoidal M) {a} ) )
146 φ●1 : { a b : Obj C } → Hom D (Monoidal.m-i N ● FObj MF b ) ( FObj MF ( Monoidal.m-i M ) ● FObj MF b ) 146 ρD : { a b : Obj C } → Hom D (F a ● Monoidal.m-i N ) ( F a )
147 φ●1 = {!!} 147 ρD {a} {b} = ≅→ (mρ-iso (isMonoidal N) {F a} )
148 φICB : { a b : Obj C } → Hom D ( FObj MF ( Monoidal.m-i M ) ● FObj MF b ) ( FObj MF ( ( Monoidal.m-i M ) ⊗ b ) ) 148 φ●1 : { a b : Obj C } → Hom D (Monoidal.m-i N ● F b ) ( F ( Monoidal.m-i M ) ● F b )
149 φICB = {!!} 149 φ●1 {a} {b} = φ ■ id1 D (F b)
150 FλD : { a b : Obj C } → Hom D ( FObj MF ( ( Monoidal.m-i M ) ⊗ b ) ) (FObj MF b ) 150 φICB : { a b : Obj C } → Hom D ( F ( Monoidal.m-i M ) ● F b ) ( F ( ( Monoidal.m-i M ) ⊗ b ) )
151 FλD = {!!} 151 φICB {a} {b} = {!!}
152 λD : { a b : Obj C } → Hom D (Monoidal.m-i N ● FObj MF b ) (FObj MF b ) 152 FλD : { a b : Obj C } → Hom D ( F ( ( Monoidal.m-i M ) ⊗ b ) ) (F b )
153 λD = {!!} 153 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 )
155 λD {a} {b} = ≅→ (mλ-iso (isMonoidal N) {F b} )
154 field 156 field
155 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 ] ] ] 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 ] ] ]
156 comm-idr : {a b : Obj C } → D [ D [ FρC {a} {b} o D [ φAIC {a} {b} o 1●φ {a} {b} ] ] ≈ ρD {a} {b} ] 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} ]
157 comm-idl : {a b : Obj C } → D [ D [ FλD {a} {b} o D [ φICB {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} ]
158 160