WithGivens for monoidal and (co)cartesian derivations

CartesianCategories/PackageInfo.g

@@ -10,7 +10,7 @@ SetPackageInfo( rec(
 
 PackageName := "CartesianCategories",
 Subtitle := "Cartesian and cocartesian categories and various subdoctrines",
-Version := "2023.11-02",
+Version := "2023.11-03",
 Date := ~.Version{[ 1 .. 10 ]},
 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)( ),
 License := "GPL-2.0-or-later",

CartesianCategories/gap/BraidedCartesianCategoriesDerivedMethods.gi

@@ -11,22 +11,23 @@
 AddDerivationToCAP( CartesianBraidingInverseWithGivenDirectProducts,
                     "CartesianBraidingInverseWithGivenDirectProducts as the inverse of the braiding",
                     [ [ InverseForMorphisms, 1 ],
-                      [ CartesianBraiding, 1 ] ],
+                      [ CartesianBraidingWithGivenDirectProducts, 1 ] ],
 
   function( cat, object_2_x_object_1, object_1, object_2, object_1_x_object_2 )
-    ##TODO: Use CartesianBraidingWithGiven
-    return InverseForMorphisms( cat, CartesianBraiding( cat, object_1, object_2 ) );
+
+    return InverseForMorphisms( cat, CartesianBraidingWithGivenDirectProducts( cat, object_1_x_object_2, object_1, object_2, object_2_x_object_1 ) );
 
 end : CategoryFilter := IsCartesianCategory );
 
 ##
 AddDerivationToCAP( CartesianBraidingWithGivenDirectProducts,
                     "CartesianBraidingWithGivenDirectProducts as the inverse of CartesianBraidingInverse",
                     [ [ InverseForMorphisms, 1 ],
-                      [ CartesianBraidingInverse, 1 ] ],
+                      [ CartesianBraidingInverseWithGivenDirectProducts, 1 ] ],
 
   function( cat, object_1_x_object_2, object_1, object_2, object_2_x_object_1 )
-    ##TODO: Use CartesianBraidingInverseWithGiven
-    return InverseForMorphisms( cat, CartesianBraidingInverse( cat, object_1, object_2 ) );
+
+    return InverseForMorphisms( cat, CartesianBraidingInverseWithGivenDirectProducts( cat, object_2_x_object_1, object_1, object_2, object_1_x_object_2 ) );
 
 end : CategoryFilter := IsCartesianCategory );
+

CartesianCategories/gap/BraidedCocartesianCategoriesDerivedMethods.gi

@@ -11,22 +11,23 @@
 AddDerivationToCAP( CocartesianBraidingInverseWithGivenCoproducts,
                     "CocartesianBraidingInverseWithGivenCoproducts as the inverse of the braiding",
                     [ [ InverseForMorphisms, 1 ],
-                      [ CocartesianBraiding, 1 ] ],
+                      [ CocartesianBraidingWithGivenCoproducts, 1 ] ],
 
   function( cat, object_2_u_object_1, object_1, object_2, object_1_u_object_2 )
-    ##TODO: Use CocartesianBraidingWithGiven
-    return InverseForMorphisms( cat, CocartesianBraiding( cat, object_1, object_2 ) );
+
+    return InverseForMorphisms( cat, CocartesianBraidingWithGivenCoproducts( cat, object_1_u_object_2, object_1, object_2, object_2_u_object_1 ) );
 
 end : CategoryFilter := IsCocartesianCategory );
 
 ##
 AddDerivationToCAP( CocartesianBraidingWithGivenCoproducts,
                     "CocartesianBraidingWithGivenCoproducts as the inverse of CocartesianBraidingInverse",
                     [ [ InverseForMorphisms, 1 ],
-                      [ CocartesianBraidingInverse, 1 ] ],
+                      [ CocartesianBraidingInverseWithGivenCoproducts, 1 ] ],
 
   function( cat, object_1_u_object_2, object_1, object_2, object_2_u_object_1 )
-    ##TODO: Use CocartesianBraidingInverseWithGiven
-    return InverseForMorphisms( cat, CocartesianBraidingInverse( cat, object_1, object_2 ) );
+
+    return InverseForMorphisms( cat, CocartesianBraidingInverseWithGivenCoproducts( cat, object_2_u_object_1, object_1, object_2, object_1_u_object_2 ) );
 
 end : CategoryFilter := IsCocartesianCategory );
+

CartesianCategories/gap/SymmetricCartesianClosedCategoriesDerivedMethods.gi

@@ -291,7 +291,7 @@
 ##
 AddDerivationToCAP( CartesianEvaluationForCartesianDualWithGivenDirectProduct,
                     "CartesianEvaluationForCartesianDualWithGivenDirectProduct using the direct product-exponential adjunction and IsomorphismFromCartesianDualObjectToExponentialIntoTerminalObject",
-                    [ [ ExponentialToDirectProductAdjunctionMap, 1 ],
+                    [ [ ExponentialToDirectProductAdjunctionMapWithGivenDirectProduct, 1 ],
                       [ IsomorphismFromCartesianDualObjectToExponentialIntoTerminalObject, 1 ] ],
 
   function( cat, s, a, r )
@@ -300,8 +300,11 @@
     #
     # Adjoint( a^v → Exp(a,1) ) = ( a^v × a → 1 )
 
-    return ExponentialToDirectProductAdjunctionMap( cat, a, r,
-                                                    IsomorphismFromCartesianDualObjectToExponentialIntoTerminalObject( cat, a ) );
+    return ExponentialToDirectProductAdjunctionMapWithGivenDirectProduct( cat,
+                a,
+                r,
+                IsomorphismFromCartesianDualObjectToExponentialIntoTerminalObject( cat, a ),
+                s );
 
 end : CategoryFilter := IsCartesianClosedCategory );
 
@@ -531,14 +534,16 @@
 AddDerivationToCAP( IsomorphismFromObjectToExponentialWithGivenExponential,
                     "IsomorphismFromObjectToExponentialWithGivenExponential using the coevaluation morphism",
                     [ [ TerminalObject, 1 ],
+                      [ DirectProduct, 1 ],
+                      [ ExponentialOnObjects, 1 ],
                       [ PreCompose, 1 ],
-                      [ CartesianCoevaluationMorphism, 1 ],
-                      [ ExponentialOnMorphisms, 1 ],
+                      [ CartesianCoevaluationMorphismWithGivenRange, 1 ],
+                      [ ExponentialOnMorphismsWithGivenExponentials, 1 ],
                       [ IdentityMorphism, 1 ],
-                      [ CartesianRightUnitor, 1 ] ],
+                      [ CartesianRightUnitorWithGivenDirectProduct, 1 ] ],
 
   function( cat, a, internal_hom )
-    local unit;
+    local unit, a_x_1, exp_1_ax1;
 
     #       a
     #       |
@@ -551,20 +556,24 @@
     #   Exp(1, a)
 
     unit := TerminalObject( cat );
+    a_x_1 := BinaryDirectProduct( cat, a, unit );
+    exp_1_ax1:= ExponentialOnObjects( cat, unit, a_x_1 );
 
     return PreCompose( cat,
-             CartesianCoevaluationMorphism( cat, a, unit ),
-             ExponentialOnMorphisms( cat,
-               IdentityMorphism( cat, unit ),
-               CartesianRightUnitor( cat, a ) ) );
+                       CartesianCoevaluationMorphismWithGivenRange( cat, a, unit, exp_1_ax1 ),
+                       ExponentialOnMorphismsWithGivenExponentials( cat,
+                               exp_1_ax1,
+                               IdentityMorphism( cat, unit ),
+                               CartesianRightUnitorWithGivenDirectProduct( cat, a, a_x_1 ),
+                               internal_hom ) );
 
 end : CategoryFilter := IsCartesianClosedCategory );
 
 ##
 AddDerivationToCAP( IsomorphismFromObjectToExponentialWithGivenExponential,
                     "IsomorphismFromObjectToExponentialWithGivenExponential as the adjoint of the right unitor",
                     [ [ TerminalObject, 1 ],
-                      [ DirectProductToExponentialAdjunctionMap, 1 ],
+                      [ DirectProductToExponentialAdjunctionMapWithGivenExponential, 1 ],
                       [ CartesianRightUnitor, 1 ] ],
 
   function( cat, a, internal_hom )
@@ -573,10 +582,11 @@
     #
     # Adjoint( ρ_a ) = ( a → Exp(1,a) )
 
-    return DirectProductToExponentialAdjunctionMap( cat,
+    return DirectProductToExponentialAdjunctionMapWithGivenExponential( cat,
                    a,
                    TerminalObject( cat ),
-                   CartesianRightUnitor( cat, a ) );
+                   CartesianRightUnitor( cat, a ),
+                   internal_hom );
 
 end : CategoryFilter := IsCartesianClosedCategory );
 
@@ -598,10 +608,13 @@
                     "IsomorphismFromExponentialToObjectWithGivenExponential using the evaluation morphism",
                     [ [ TerminalObject, 1 ],
                       [ PreCompose, 1 ],
-                      [ CartesianRightUnitorInverse, 1 ],
-                      [ CartesianEvaluationMorphism, 1 ] ],
+                      [ DirectProduct, 1 ],
+                      [ ExponentialOnObjects, 1 ],
+                      [ CartesianRightUnitorInverseWithGivenDirectProduct, 1 ],
+                      [ CartesianEvaluationMorphismWithGivenSource, 1 ] ],
 
   function( cat, a, internal_hom )
+    local unit, exp_1a, exp_1a_x_1;
 
     #  Exp(1,a)
     #      |
@@ -613,9 +626,13 @@
     #      v
     #      a
 
+    unit := TerminalObject( cat );
+    exp_1a := ExponentialOnObjects( cat, unit, a );
+    exp_1a_x_1 := BinaryDirectProduct( cat, exp_1a, unit );
+
     return PreCompose( cat,
-                   CartesianRightUnitorInverse( cat, internal_hom ),
-                   CartesianEvaluationMorphism( cat, TerminalObject( cat ), a ) );
+                       CartesianRightUnitorInverseWithGivenDirectProduct( cat, internal_hom, exp_1a_x_1 ),
+                       CartesianEvaluationMorphismWithGivenSource( cat, unit, a, exp_1a_x_1 ) );
 
 end : CategoryFilter := IsCartesianClosedCategory );
 
@@ -682,34 +699,38 @@
 ##
 AddDerivationToCAP( CartesianEvaluationMorphismWithGivenSource,
                     "CartesianEvaluationMorphismWithGivenSource using the direct product-exponential adjunction on the identity",
-                    [ [ ExponentialToDirectProductAdjunctionMap, 1 ],
+                    [ [ ExponentialToDirectProductAdjunctionMapWithGivenDirectProduct, 1 ],
                       [ IdentityMorphism, 1 ],
                       [ ExponentialOnObjects, 1 ] ],
 
   function( cat, a, b, direct_product_object )
 
     # Adjoint( id_Exp(a,b): Exp(a,b) → Exp(a,b) ) = ( Exp(a,b) × a → b )
 
-    return ExponentialToDirectProductAdjunctionMap( cat,
-             a, b,
-             IdentityMorphism( cat, ExponentialOnObjects( cat, a, b ) ) );
+    return ExponentialToDirectProductAdjunctionMapWithGivenDirectProduct( cat,
+             a,
+             b,
+             IdentityMorphism( cat, ExponentialOnObjects( cat, a, b ) ),
+             direct_product_object );
 
 end : CategoryFilter := IsCartesianClosedCategory );
 
 ##
 AddDerivationToCAP( CartesianCoevaluationMorphismWithGivenRange,
                     "CartesianCoevaluationMorphismWithGivenRange using the direct product-exponential adjunction on the identity",
-                    [ [ DirectProductToExponentialAdjunctionMap, 1 ],
+                    [ [ DirectProductToExponentialAdjunctionMapWithGivenExponential, 1 ],
                       [ IdentityMorphism, 1 ],
                       [ DirectProduct, 1 ] ],
 
   function( cat, a, b, internal_hom )
 
     # Adjoint( id_(a × b): a × b → a × b ) = ( a → Exp(b, a × b) )
 
-    return DirectProductToExponentialAdjunctionMap( cat,
-             a, b,
-             IdentityMorphism( cat, BinaryDirectProduct( cat, a, b ) ) );
+    return DirectProductToExponentialAdjunctionMapWithGivenExponential( cat,
+             a,
+             b,
+             IdentityMorphism( cat, BinaryDirectProduct( cat, a, b ) ),
+             internal_hom );
 
 end : CategoryFilter := IsCartesianClosedCategory );
 
@@ -852,13 +873,14 @@
 ##
 AddDerivationToCAP( CartesianPostComposeMorphismWithGivenObjects,
                     "CartesianPostComposeMorphismWithGivenObjects using CartesianPreComposeMorphism and braiding",
-                    [ [ CartesianBraiding, 1 ],
+                    [ [ CartesianBraidingWithGivenDirectProducts, 1 ],
                       [ ExponentialOnObjects, 2 ],
                       [ PreCompose, 1 ],
-                      [ CartesianPreComposeMorphism, 1 ] ],
+                      [ DirectProduct, 1],
+                      [ CartesianPreComposeMorphismWithGivenObjects, 1 ] ],
 
   function( cat, source, a, b, c, range )
-    local braiding;
+    local exp_ab, exp_bc, exp_ab_x_exp_bc, braiding;
 
     # Exp(b,c) × Exp(a,b)
     #          |
@@ -870,22 +892,27 @@
     #          v
     #       Exp(a,c)
 
-    braiding := CartesianBraiding( cat, ExponentialOnObjects( cat, b, c ), ExponentialOnObjects( cat, a, b ) );
+    exp_ab := ExponentialOnObjects( cat, a, b );
+    exp_bc := ExponentialOnObjects( cat, b, c );
+    exp_ab_x_exp_bc := BinaryDirectProduct( cat, exp_ab, exp_bc );
+
+    braiding := CartesianBraidingWithGivenDirectProducts( cat, source, exp_bc, exp_ab, exp_ab_x_exp_bc );
 
-    return PreCompose( cat, braiding, CartesianPreComposeMorphism( cat, a, b, c ) );
+    return PreCompose( cat, braiding, CartesianPreComposeMorphismWithGivenObjects( cat, exp_ab_x_exp_bc, a, b, c, range ) );
 
 end : CategoryFilter := IsCartesianClosedCategory );
 
 ##
 AddDerivationToCAP( CartesianPreComposeMorphismWithGivenObjects,
                     "CartesianPreComposeMorphismWithGivenObjects using CartesianPostComposeMorphism and braiding",
-                    [ [ CartesianBraiding, 1 ],
+                    [ [ CartesianBraidingWithGivenDirectProducts, 1 ],
                       [ ExponentialOnObjects, 2 ],
                       [ PreCompose, 1 ],
-                      [ CartesianPostComposeMorphism, 1 ] ],
+                      [ DirectProduct, 1],
+                      [ CartesianPostComposeMorphismWithGivenObjects, 1 ] ],
 
   function( cat, source, a, b, c, range )
-    local braiding;
+    local exp_ab, exp_bc, exp_bc_x_exp_ab, braiding;
 
     # Exp(a,b) × Exp(b,c)
     #          |
@@ -897,9 +924,13 @@
     #          v
     #       Exp(a,c)
 
-    braiding := CartesianBraiding( cat, ExponentialOnObjects( cat, a, b ), ExponentialOnObjects( cat, b, c ) );
+    exp_ab := ExponentialOnObjects( cat, a, b );
+    exp_bc := ExponentialOnObjects( cat, b, c );
+    exp_bc_x_exp_ab := BinaryDirectProduct( cat, exp_bc, exp_ab );
+
+    braiding := CartesianBraidingWithGivenDirectProducts( cat, source, exp_bc, exp_ab, exp_bc_x_exp_ab );
 
-    return PreCompose( cat, braiding, CartesianPostComposeMorphism( cat, a, b, c ) );
+    return PreCompose( cat, braiding, CartesianPostComposeMorphismWithGivenObjects( cat, exp_bc_x_exp_ab, a, b, c, range ) );
 
 end : CategoryFilter := IsCartesianClosedCategory );