|
7 | 7 |
|
8 | 8 |
|
9 | 9 |
|
| 10 | +## |
| 11 | +InstallMethod( TestZigzagOfCartesianRightDirectProduct, |
| 12 | + [ IsCapCategory, IsCapCategoryObject, IsCapCategoryObject ], |
| 13 | + |
| 14 | + function( cat, a, b ) |
| 15 | + |
| 16 | + return IsOne( cat, |
| 17 | + PreCompose( cat, |
| 18 | + DirectProductOnObjectAndMorphism( cat, |
| 19 | + a, |
| 20 | + CartesianRightCoevaluationMorphism( cat, a, b ) ), |
| 21 | + CartesianRightEvaluationMorphism( cat, |
| 22 | + a, |
| 23 | + BinaryDirectProduct( cat, a, b ) ) ) ); |
| 24 | + |
| 25 | +end ); |
| 26 | + |
| 27 | +## |
| 28 | +InstallMethod( TestZigzagOfCartesianRightExponential, |
| 29 | + [ IsCapCategory, IsCapCategoryObject, IsCapCategoryObject ], |
| 30 | + |
| 31 | + function( cat, a, b ) |
| 32 | + |
| 33 | + return IsOne( cat, |
| 34 | + PreCompose( cat, |
| 35 | + CartesianRightCoevaluationMorphism( cat, |
| 36 | + a, |
| 37 | + ExponentialOnObjects( cat, |
| 38 | + a, |
| 39 | + b ) ), |
| 40 | + ExponentialOnMorphisms( cat, |
| 41 | + IdentityMorphism( a ), |
| 42 | + CartesianRightEvaluationMorphism( cat, |
| 43 | + a, |
| 44 | + b ) ) ) ); |
| 45 | + |
| 46 | +end ); |
| 47 | + |
| 48 | +## |
| 49 | +InstallMethod( TestZigzagOfCartesianLeftDirectProduct, |
| 50 | + [ IsCapCategory, IsCapCategoryObject, IsCapCategoryObject ], |
| 51 | + |
| 52 | + function( cat, a, b ) |
| 53 | + |
| 54 | + return IsOne( cat, |
| 55 | + PreCompose( cat, |
| 56 | + DirectProductOnMorphismAndObject( cat, |
| 57 | + CartesianLeftCoevaluationMorphism( cat, a, b ), |
| 58 | + a ), |
| 59 | + CartesianLeftEvaluationMorphism( cat, |
| 60 | + a, |
| 61 | + BinaryDirectProduct( cat, b, a ) ) ) ); |
| 62 | + |
| 63 | +end ); |
| 64 | + |
| 65 | +## |
| 66 | +InstallMethod( TestZigzagOfCartesianLeftExponential, |
| 67 | + [ IsCapCategory, IsCapCategoryObject, IsCapCategoryObject ], |
| 68 | + |
| 69 | + function( cat, a, b ) |
| 70 | + |
| 71 | + return IsOne( cat, |
| 72 | + PreCompose( cat, |
| 73 | + CartesianLeftCoevaluationMorphism( cat, |
| 74 | + a, |
| 75 | + ExponentialOnObjects( cat, |
| 76 | + a, |
| 77 | + b ) ), |
| 78 | + ExponentialOnMorphisms( cat, |
| 79 | + IdentityMorphism( a ), |
| 80 | + CartesianLeftEvaluationMorphism( cat, |
| 81 | + a, |
| 82 | + b ) ) ) ); |
| 83 | + |
| 84 | +end ); |
| 85 | + |
| 86 | +## |
10 | 87 | InstallGlobalFunction( "CartesianClosedCategoriesTest", |
11 | 88 |
|
12 | 89 | function( cat, opposite, a, b, c, d, alpha, beta, gamma, delta, epsilon, zeta ) |
@@ -172,14 +249,14 @@ InstallGlobalFunction( "CartesianClosedCategoriesTest", |
172 | 249 | fi; |
173 | 250 |
|
174 | 251 | if CanCompute( cat, "CartesianRightCoevaluationMorphism" ) then |
175 | | - |
| 252 | + |
176 | 253 | if verbose then |
177 | | - |
| 254 | + |
178 | 255 | # COVERAGE_IGNORE_NEXT_LINE |
179 | 256 | Display( "Testing 'CartesianRightEvaluationMorphism' ..." ); |
180 | | - |
| 257 | + |
181 | 258 | fi; |
182 | | - |
| 259 | + |
183 | 260 | coev_ab := CartesianRightCoevaluationMorphism( a, b ); |
184 | 261 | coev_ba := CartesianRightCoevaluationMorphism( b, a ); |
185 | 262 |
|
@@ -232,6 +309,52 @@ InstallGlobalFunction( "CartesianClosedCategoriesTest", |
232 | 309 |
|
233 | 310 | fi; |
234 | 311 |
|
| 312 | + if CanCompute( cat, "CartesianRightCoevaluationMorphism" ) and |
| 313 | + CanCompute( cat, "CartesianRightEvaluationMorphism" ) then |
| 314 | + |
| 315 | + if verbose then |
| 316 | + |
| 317 | + # COVERAGE_IGNORE_NEXT_LINE |
| 318 | + Display( "Testing 'TestZigzagOfCartesianRightDirectProduct' ..." ); |
| 319 | + |
| 320 | + fi; |
| 321 | + |
| 322 | + Assert( 0, TestZigzagOfCartesianRightDirectProduct( cat, a, b ) ); |
| 323 | + |
| 324 | + if verbose then |
| 325 | + |
| 326 | + # COVERAGE_IGNORE_NEXT_LINE |
| 327 | + Display( "Testing 'TestZigzagOfCartesianRightExponential' ..." ); |
| 328 | + |
| 329 | + fi; |
| 330 | + |
| 331 | + Assert( 0, TestZigzagOfCartesianRightExponential( cat, a, b ) ); |
| 332 | + |
| 333 | + fi; |
| 334 | + |
| 335 | + if CanCompute( cat, "CartesianLeftCoevaluationMorphism" ) and |
| 336 | + CanCompute( cat, "CartesianLeftEvaluationMorphism" ) then |
| 337 | + |
| 338 | + if verbose then |
| 339 | + |
| 340 | + # COVERAGE_IGNORE_NEXT_LINE |
| 341 | + Display( "Testing 'TestZigzagOfCartesianLeftDirectProduct' ..." ); |
| 342 | + |
| 343 | + fi; |
| 344 | + |
| 345 | + Assert( 0, TestZigzagOfCartesianLeftDirectProduct( cat, a, b ) ); |
| 346 | + |
| 347 | + if verbose then |
| 348 | + |
| 349 | + # COVERAGE_IGNORE_NEXT_LINE |
| 350 | + Display( "Testing 'TestZigzagOfCartesianLeftExponential' ..." ); |
| 351 | + |
| 352 | + fi; |
| 353 | + |
| 354 | + Assert( 0, TestZigzagOfCartesianLeftExponential( cat, a, b ) ); |
| 355 | + |
| 356 | + fi; |
| 357 | + |
235 | 358 | if CanCompute( cat, "DirectProductToExponentialRightAdjunctionIsomorphism" ) then |
236 | 359 |
|
237 | 360 | if verbose then |
|
0 commit comments