Skip to content

Commit f1bfdd4

Browse files
Merge pull request #1866 from mohamed-barakat/ClosedMonoidalTests
test zigzags for closed structures
2 parents 309bc9e + 88252a1 commit f1bfdd4

12 files changed

Lines changed: 391 additions & 49 deletions

CartesianCategories/PackageInfo.g

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ SetPackageInfo( rec(
1010

1111
PackageName := "CartesianCategories",
1212
Subtitle := "Cartesian and cocartesian categories and various subdoctrines",
13-
Version := "2026.07-01",
13+
Version := "2026.07-02",
1414
Date := ~.Version{[ 1 .. 10 ]},
1515
Date := (function ( ) if IsBound( GAPInfo.SystemEnvironment.GAP_PKG_RELEASE_DATE ) then return GAPInfo.SystemEnvironment.GAP_PKG_RELEASE_DATE; else return Concatenation( ~.Version{[ 1 .. 4 ]}, "-", ~.Version{[ 6, 7 ]}, "-01" ); fi; end)( ),
1616
License := "GPL-2.0-or-later",
@@ -99,7 +99,7 @@ Dependencies := rec(
9999
GAP := ">= 4.13.0",
100100
NeededOtherPackages := [
101101
[ "CAP", ">= 2026.06-01" ],
102-
[ "MonoidalCategories", ">= 2026.06-01" ],
102+
[ "MonoidalCategories", ">= 2026.07-02" ],
103103
],
104104
SuggestedOtherPackages := [ ],
105105
ExternalConditions := [ ],
Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,3 @@
11
The files of this package which include the line `THIS FILE WAS AUTOMATICALLY GENERATED` in their header have been autogenerated
22

3-
* from MonoidalCategories v2026.06-01
3+
* from MonoidalCategories v2026.07-02

CartesianCategories/gap/CartesianCategoriesTest.gd

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@
1313

1414
#! @Description
1515
#! This is a debug operation.
16-
#! The arguments are two objects $obj$ in a cartesian category $cat$.
16+
#! The arguments are a cartesian category $cat$ and an object $obj$ therein.
1717
#! The output is true if the left and right unitors are invertible for $obj$.
1818
#! @Returns a boolean
1919
#! @Arguments cat, obj
@@ -22,27 +22,27 @@ DeclareOperation( "TestCartesianUnitorsForInvertibility",
2222

2323
#! @Description
2424
#! This is a debug operation.
25-
#! The arguments are two objects $obj_1, obj_2, obj_3$ in a cartesian category $cat$.
25+
#! The arguments are a cartesian category $cat$ and three objects $obj_1, obj_2, obj_3$ therein.
2626
#! The output is true if the associator are invertible
27-
#! for these 3 objects, false otherwise.
27+
#! for these three objects, false otherwise.
2828
#! @Returns a boolean
2929
#! @Arguments cat, obj_1, obj_2, obj_3
3030
DeclareOperation( "TestCartesianAssociatorForInvertibility",
3131
[ IsCapCategory, IsCapCategoryObject, IsCapCategoryObject, IsCapCategoryObject ] );
3232

3333
#! @Description
3434
#! This is a debug operation.
35-
#! The arguments are two objects $obj_1, obj_2$ in a cartesian category $cat$.
35+
#! The arguments are a cartesian category $cat$ and two objects $obj_1, obj_2$ therein.
3636
#! The output is true if the triangle identity holds
37-
#! for these 2 objects, false otherwise.
37+
#! for these two objects, false otherwise.
3838
#! @Returns a boolean
3939
#! @Arguments cat, obj_1, obj_2
4040
DeclareOperation( "TestCartesianTriangleIdentity",
4141
[ IsCapCategory, IsCapCategoryObject, IsCapCategoryObject ] );
4242

4343
#! @Description
4444
#! This is a debug operation.
45-
#! The argument is a list $L$ of objects in a cartesian category $cat$.
45+
#! The arguments are a cartesian category $cat$ and a list $L$ of objects therein.
4646
#! The output is true if the triangle identity holds
4747
#! for all pairs of objects in $L$, otherwise false.
4848
#! @Returns a boolean
@@ -51,19 +51,19 @@ DeclareOperation( "TestCartesianTriangleIdentityForAllPairsInList", [ IsCapCateg
5151

5252
#! @Description
5353
#! This is a debug operation.
54-
#! The arguments are 4 objects $obj_1, obj_2, obj_3, obj_4$ in a cartesian category $cat$.
54+
#! The arguments are a cartesian category $cat$ and four objects $obj_1, obj_2, obj_3, obj_4$ therein.
5555
#! The output is true if the pentagon identity holds
56-
#! for these 4 objects, false otherwise.
56+
#! for these four objects, false otherwise.
5757
#! @Returns a boolean
5858
#! @Arguments cat, obj_1, obj_2, obj_3, obj_4
5959
DeclareOperation( "TestCartesianPentagonIdentity",
6060
[ IsCapCategory, IsCapCategoryObject, IsCapCategoryObject, IsCapCategoryObject, IsCapCategoryObject ] );
6161

6262
#! @Description
6363
#! This is a debug operation.
64-
#! The arguments are 4 objects $obj_1, obj_2, obj_3, obj_4$ in a cartesian category $cat$.
64+
#! The arguments are a cartesian category $cat$ and four objects $obj_1, obj_2, obj_3, obj_4$ therein.
6565
#! The output is true if the pentagon identity holds
66-
#! for these 4 objects, false otherwise.
66+
#! for these four objects, false otherwise.
6767
#! This test uses the WithGiven-operations.
6868
#! @Returns a boolean
6969
#! @Arguments cat, obj_1, obj_2, obj_3, obj_4
@@ -72,7 +72,7 @@ DeclareOperation( "TestCartesianPentagonIdentityUsingWithGivenOperations",
7272

7373
#! @Description
7474
#! This is a debug operation.
75-
#! The argument is a list $L$ of objects in a cartesian category $cat$.
75+
#! The arguments are a cartesian category $cat$ and a list $L$ of objects therein.
7676
#! The output is true if the pentagon identity holds
7777
#! for all quadruples of objects in $L$, otherwise false.
7878
#! @Returns a boolean

CartesianCategories/gap/CartesianClosedCategoriesTest.gd

Lines changed: 48 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,54 @@
1111

1212
#! @Section Test functions
1313

14+
#! @Description
15+
#! This is a debug operation.
16+
#! The arguments are a cartesian category $cat$ and two objects $a$, $b$ therein.
17+
#! The output is true if the zigzag rule
18+
#! $L(b) \to (LRL)(b) \to L(b) = id_b$ is satisfied for
19+
#! * $L = a \times -$,
20+
#! * $R = \mathrm{Hom}(a, -)$.
21+
#! @Returns a boolean
22+
#! @Arguments cat, a, b
23+
DeclareOperation( "TestZigzagOfCartesianRightDirectProduct",
24+
[ IsCapCategory, IsCapCategoryObject, IsCapCategoryObject ] );
25+
26+
#! @Description
27+
#! This is a debug operation.
28+
#! The arguments are a cartesian category $cat$ and two objects $a$, $b$ therein.
29+
#! The output is true if the zigzag rule
30+
#! $R(b) \to (RLR)(b) \to R(b) = id_b$ is satisfied for
31+
#! * $L = a \times -$,
32+
#! * $R = \mathrm{Hom}(a, -)$.
33+
#! @Returns a boolean
34+
#! @Arguments cat, a, b
35+
DeclareOperation( "TestZigzagOfCartesianRightExponential",
36+
[ IsCapCategory, IsCapCategoryObject, IsCapCategoryObject ] );
37+
38+
#! @Description
39+
#! This is a debug operation.
40+
#! The arguments are a cartesian category $cat$ and two objects $a$, $b$ therein.
41+
#! The output is true if the zigzag rule
42+
#! $L(b) \to (LRL)(b) \to L(b) = id_b$ is satisfied for
43+
#! * $L = - \times a$,
44+
#! * $R = \mathrm{Hom}(a, -)$.
45+
#! @Returns a boolean
46+
#! @Arguments cat, a, b
47+
DeclareOperation( "TestZigzagOfCartesianLeftDirectProduct",
48+
[ IsCapCategory, IsCapCategoryObject, IsCapCategoryObject ] );
49+
50+
#! @Description
51+
#! This is a debug operation.
52+
#! The arguments are a cartesian category $cat$ and two objects $a$, $b$ therein.
53+
#! The output is true if the zigzag rule
54+
#! $R(b) \to (RLR)(b) \to R(b) = id_b$ is satisfied for
55+
#! * $L = - \times a$,
56+
#! * $R = \mathrm{Hom}(a, -)$.
57+
#! @Returns a boolean
58+
#! @Arguments cat, a, b
59+
DeclareOperation( "TestZigzagOfCartesianLeftExponential",
60+
[ IsCapCategory, IsCapCategoryObject, IsCapCategoryObject ] );
61+
1462
#! @Description
1563
#! The arguments are
1664
#! * a CAP category $cat$

CartesianCategories/gap/CartesianClosedCategoriesTest.gi

Lines changed: 127 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,83 @@
77

88

99

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+
##
1087
InstallGlobalFunction( "CartesianClosedCategoriesTest",
1188

1289
function( cat, opposite, a, b, c, d, alpha, beta, gamma, delta, epsilon, zeta )
@@ -172,14 +249,14 @@ InstallGlobalFunction( "CartesianClosedCategoriesTest",
172249
fi;
173250

174251
if CanCompute( cat, "CartesianRightCoevaluationMorphism" ) then
175-
252+
176253
if verbose then
177-
254+
178255
# COVERAGE_IGNORE_NEXT_LINE
179256
Display( "Testing 'CartesianRightEvaluationMorphism' ..." );
180-
257+
181258
fi;
182-
259+
183260
coev_ab := CartesianRightCoevaluationMorphism( a, b );
184261
coev_ba := CartesianRightCoevaluationMorphism( b, a );
185262

@@ -232,6 +309,52 @@ InstallGlobalFunction( "CartesianClosedCategoriesTest",
232309

233310
fi;
234311

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+
235358
if CanCompute( cat, "DirectProductToExponentialRightAdjunctionIsomorphism" ) then
236359

237360
if verbose then

CartesianCategories/gap/CocartesianCategoriesTest.gd

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@
1313

1414
#! @Description
1515
#! This is a debug operation.
16-
#! The arguments are two objects $obj$ in a cocartesian category $cat$.
16+
#! The arguments are a cocartesian category $cat$ and an object $obj$ therein.
1717
#! The output is true if the left and right unitors are invertible for $obj$.
1818
#! @Returns a boolean
1919
#! @Arguments cat, obj
@@ -22,27 +22,27 @@ DeclareOperation( "TestCocartesianUnitorsForInvertibility",
2222

2323
#! @Description
2424
#! This is a debug operation.
25-
#! The arguments are two objects $obj_1, obj_2, obj_3$ in a cocartesian category $cat$.
25+
#! The arguments are a cocartesian category $cat$ and three objects $obj_1, obj_2, obj_3$ therein.
2626
#! The output is true if the associator are invertible
27-
#! for these 3 objects, false otherwise.
27+
#! for these three objects, false otherwise.
2828
#! @Returns a boolean
2929
#! @Arguments cat, obj_1, obj_2, obj_3
3030
DeclareOperation( "TestCocartesianAssociatorForInvertibility",
3131
[ IsCapCategory, IsCapCategoryObject, IsCapCategoryObject, IsCapCategoryObject ] );
3232

3333
#! @Description
3434
#! This is a debug operation.
35-
#! The arguments are two objects $obj_1, obj_2$ in a cocartesian category $cat$.
35+
#! The arguments are a cocartesian category $cat$ and two objects $obj_1, obj_2$ therein.
3636
#! The output is true if the triangle identity holds
37-
#! for these 2 objects, false otherwise.
37+
#! for these two objects, false otherwise.
3838
#! @Returns a boolean
3939
#! @Arguments cat, obj_1, obj_2
4040
DeclareOperation( "TestCocartesianTriangleIdentity",
4141
[ IsCapCategory, IsCapCategoryObject, IsCapCategoryObject ] );
4242

4343
#! @Description
4444
#! This is a debug operation.
45-
#! The argument is a list $L$ of objects in a cocartesian category $cat$.
45+
#! The arguments are a cocartesian category $cat$ and a list $L$ of objects therein.
4646
#! The output is true if the triangle identity holds
4747
#! for all pairs of objects in $L$, otherwise false.
4848
#! @Returns a boolean
@@ -51,19 +51,19 @@ DeclareOperation( "TestCocartesianTriangleIdentityForAllPairsInList", [ IsCapCat
5151

5252
#! @Description
5353
#! This is a debug operation.
54-
#! The arguments are 4 objects $obj_1, obj_2, obj_3, obj_4$ in a cocartesian category $cat$.
54+
#! The arguments are a cocartesian category $cat$ and four objects $obj_1, obj_2, obj_3, obj_4$ therein.
5555
#! The output is true if the pentagon identity holds
56-
#! for these 4 objects, false otherwise.
56+
#! for these four objects, false otherwise.
5757
#! @Returns a boolean
5858
#! @Arguments cat, obj_1, obj_2, obj_3, obj_4
5959
DeclareOperation( "TestCocartesianPentagonIdentity",
6060
[ IsCapCategory, IsCapCategoryObject, IsCapCategoryObject, IsCapCategoryObject, IsCapCategoryObject ] );
6161

6262
#! @Description
6363
#! This is a debug operation.
64-
#! The arguments are 4 objects $obj_1, obj_2, obj_3, obj_4$ in a cocartesian category $cat$.
64+
#! The arguments are a cocartesian category $cat$ and four objects $obj_1, obj_2, obj_3, obj_4$ therein.
6565
#! The output is true if the pentagon identity holds
66-
#! for these 4 objects, false otherwise.
66+
#! for these four objects, false otherwise.
6767
#! This test uses the WithGiven-operations.
6868
#! @Returns a boolean
6969
#! @Arguments cat, obj_1, obj_2, obj_3, obj_4
@@ -72,7 +72,7 @@ DeclareOperation( "TestCocartesianPentagonIdentityUsingWithGivenOperations",
7272

7373
#! @Description
7474
#! This is a debug operation.
75-
#! The argument is a list $L$ of objects in a cocartesian category $cat$.
75+
#! The arguments are a cocartesian category $cat$ and a list $L$ of objects therein.
7676
#! The output is true if the pentagon identity holds
7777
#! for all quadruples of objects in $L$, otherwise false.
7878
#! @Returns a boolean

MonoidalCategories/PackageInfo.g

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ SetPackageInfo( rec(
1010

1111
PackageName := "MonoidalCategories",
1212
Subtitle := "Monoidal and monoidal (co)closed categories",
13-
Version := "2026.06-02",
13+
Version := "2026.07-02",
1414
Date := (function ( ) if IsBound( GAPInfo.SystemEnvironment.GAP_PKG_RELEASE_DATE ) then return GAPInfo.SystemEnvironment.GAP_PKG_RELEASE_DATE; else return Concatenation( ~.Version{[ 1 .. 4 ]}, "-", ~.Version{[ 6, 7 ]}, "-01" ); fi; end)( ),
1515
License := "GPL-2.0-or-later",
1616

0 commit comments

Comments
 (0)