Add UniversalPropertyOf(Co)DualWithGiven(Co)DualObject

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/AUTOGENERATED_FROM.md

@@ -1,3 +1,3 @@
 The files of this package which include the line `THIS FILE WAS AUTOMATICALLY GENERATED` in their header have been autogenerated
 
-* from MonoidalCategories v2023.11-02
+* from MonoidalCategories v2023.11-03

CartesianCategories/gap/CartesianClosedCategories.autogen.gd

@@ -711,3 +711,22 @@ DeclareOperation( "AddUniversalPropertyOfCartesianDual",
 
 DeclareOperation( "AddUniversalPropertyOfCartesianDual",
                   [ IsCapCategory, IsList ] );
+
+#! @Description
+#! The arguments are a category $C$ and a function $F$.
+#! This operation adds the given function $F$
+#! to the category for the basic operation `UniversalPropertyOfCartesianDualWithGivenCartesianDualObject`.
+#! $F: ( t, a, alpha, d ) \mapsto \mathtt{UniversalPropertyOfCartesianDualWithGivenCartesianDualObject}(t, a, alpha, d)$.
+#! @Returns nothing
+#! @Arguments C, F
+DeclareOperation( "AddUniversalPropertyOfCartesianDualWithGivenCartesianDualObject",
+                  [ IsCapCategory, IsFunction ] );
+
+DeclareOperation( "AddUniversalPropertyOfCartesianDualWithGivenCartesianDualObject",
+                  [ IsCapCategory, IsFunction, IsInt ] );
+
+DeclareOperation( "AddUniversalPropertyOfCartesianDualWithGivenCartesianDualObject",
+                  [ IsCapCategory, IsList, IsInt ] );
+
+DeclareOperation( "AddUniversalPropertyOfCartesianDualWithGivenCartesianDualObject",
+                  [ IsCapCategory, IsList ] );

CartesianCategories/gap/CartesianClosedCategories.gd

@@ -317,6 +317,17 @@ DeclareAttribute( "IsomorphismFromExponentialIntoTerminalObjectToCartesianDualOb
 DeclareOperation( "UniversalPropertyOfCartesianDual",
                   [ IsCapCategoryObject, IsCapCategoryObject, IsCapCategoryMorphism ] );
 
+#! @Description
+#! The arguments are two objects $t,a$,
+#! a morphism $\alpha: t \times a \rightarrow 1$ and
+#! the dual object $d = a^{\vee}$.
+#! The output is the morphism $t \rightarrow a^{\vee}$
+#! given by the universal property of $a^{\vee}$.
+#! @Returns a morphism in $\mathrm{Hom}(t, a^{\vee})$.
+#! @Arguments t, a, alpha, d
+DeclareOperation( "UniversalPropertyOfCartesianDualWithGivenCartesianDualObject",
+                  [ IsCapCategoryObject, IsCapCategoryObject, IsCapCategoryMorphism, IsCapCategoryObject ] );
+
 #! @Description
 #! The argument is a morphism $\alpha: a \rightarrow b$.
 #! The output is the corresponding morphism $1 \rightarrow \mathrm{Exponential}(a,b)$

CartesianCategories/gap/CartesianClosedCategoriesMethodRecord.gi

@@ -403,6 +403,18 @@ UniversalPropertyOfCartesianDual := rec(
   # Test in CartesianClosedCategoriesTest
 ),
 
+UniversalPropertyOfCartesianDualWithGivenCartesianDualObject:= rec(
+  filter_list := [ "category", "object", "object", "morphism", "object" ],
+  input_arguments_names := [ "cat", "t", "a", "alpha", "d" ],
+  output_source_getter_string := "t",
+  output_source_getter_preconditions := [ ],
+  output_range_getter_string := "d",
+  output_range_getter_preconditions := [ ],
+  return_type := "morphism",
+  dual_operation := "UniversalPropertyOfCocartesianDualWithGivenCocartesianDualObject",
+  dual_arguments_reversed := false,
+),
+
 CartesianLambdaIntroduction := rec(
   filter_list := [ "category", "morphism" ],
   return_type := "morphism",

CartesianCategories/gap/CocartesianCoclosedCategories.autogen.gd

@@ -711,3 +711,22 @@ DeclareOperation( "AddUniversalPropertyOfCocartesianDual",
 
 DeclareOperation( "AddUniversalPropertyOfCocartesianDual",
                   [ IsCapCategory, IsList ] );
+
+#! @Description
+#! The arguments are a category $C$ and a function $F$.
+#! This operation adds the given function $F$
+#! to the category for the basic operation `UniversalPropertyOfCocartesianDualWithGivenCocartesianDualObject`.
+#! $F: ( t, a, alpha, c ) \mapsto \mathtt{UniversalPropertyOfCocartesianDualWithGivenCocartesianDualObject}(t, a, alpha, c)$.
+#! @Returns nothing
+#! @Arguments C, F
+DeclareOperation( "AddUniversalPropertyOfCocartesianDualWithGivenCocartesianDualObject",
+                  [ IsCapCategory, IsFunction ] );
+
+DeclareOperation( "AddUniversalPropertyOfCocartesianDualWithGivenCocartesianDualObject",
+                  [ IsCapCategory, IsFunction, IsInt ] );
+
+DeclareOperation( "AddUniversalPropertyOfCocartesianDualWithGivenCocartesianDualObject",
+                  [ IsCapCategory, IsList, IsInt ] );
+
+DeclareOperation( "AddUniversalPropertyOfCocartesianDualWithGivenCocartesianDualObject",
+                  [ IsCapCategory, IsList ] );

CartesianCategories/gap/CocartesianCoclosedCategories.gd

@@ -314,6 +314,17 @@ DeclareAttribute( "IsomorphismFromCoexponentialFromInitialObjectToCocartesianDua
 DeclareOperation( "UniversalPropertyOfCocartesianDual",
                   [ IsCapCategoryObject, IsCapCategoryObject, IsCapCategoryMorphism ] );
 
+#! @Description
+#! The arguments are two objects $t,a$,
+#! a morphism $\alpha: 1 \rightarrow t \sqcup a$ and
+#! the codual object $c = a_{\vee}$.
+#! The output is the morphism $a_{\vee} \rightarrow t$
+#! given by the universal property of $a_{\vee}$.
+#! @Returns a morphism in $\mathrm{Hom}(a_{\vee}, t)$.
+#! @Arguments t, a, alpha, c
+DeclareOperation( "UniversalPropertyOfCocartesianDualWithGivenCocartesianDualObject",
+                  [ IsCapCategoryObject, IsCapCategoryObject, IsCapCategoryMorphism, IsCapCategoryObject] );
+
 #! @Description
 #! The argument is a morphism $\alpha: a \rightarrow b$.
 #! The output is the corresponding morphism $ \mathrm{Coexponential}(a,b) \rightarrow 1$

CartesianCategories/gap/CocartesianCoclosedCategoriesMethodRecord.gi

@@ -403,6 +403,18 @@ UniversalPropertyOfCocartesianDual := rec(
   # Test in CocartesianCoclosedCategoriesTest
 ),
 
+UniversalPropertyOfCocartesianDualWithGivenCocartesianDualObject := rec(
+  filter_list := [ "category", "object", "object", "morphism", "object" ],
+  input_arguments_names := [ "cat", "t", "a", "alpha", "c" ],
+  output_source_getter_string := "c",
+  output_source_getter_preconditions := [ ],
+  output_range_getter_string := "t",
+  output_range_getter_preconditions := [ ],
+  return_type := "morphism",
+  dual_operation := "UniversalPropertyOfCartesianDualWithGivenCartesianDualObject",
+  dual_arguments_reversed := false,
+),
+
 CocartesianLambdaIntroduction := rec(
   filter_list := [ "category", "morphism" ],
   return_type := "morphism",

CartesianCategories/gap/SymmetricCartesianClosedCategoriesDerivedMethods.gi

@@ -151,7 +151,7 @@ AddDerivationToCAP( MorphismToCartesianBidualWithGivenCartesianBidual,
                       [ CartesianBraiding, 1 ],
                       [ CartesianDualOnObjects, 2 ],
                       [ CartesianEvaluationForCartesianDual, 1 ],
-                      [ UniversalPropertyOfCartesianDual, 1 ] ],
+                      [ UniversalPropertyOfCartesianDualWithGivenCartesianDualObject, 1 ] ],
 
   function( cat, a, avv )
     local alpha;
@@ -171,7 +171,7 @@ AddDerivationToCAP( MorphismToCartesianBidualWithGivenCartesianBidual,
     alpha := PreCompose( cat, CartesianBraiding( cat, a, CartesianDualOnObjects( cat, a ) ),
                             CartesianEvaluationForCartesianDual( cat, a ) );
 
-    return UniversalPropertyOfCartesianDual( cat, a, CartesianDualOnObjects( cat, a ), alpha );
+    return UniversalPropertyOfCartesianDualWithGivenCartesianDualObject( cat, a, CartesianDualOnObjects( cat, a ), alpha, avv );
 
 end : CategoryFilter := IsCartesianClosedCategory );
 

CartesianCategories/gap/SymmetricCocartesianCoclosedCategoriesDerivedMethods.gi

@@ -151,7 +151,7 @@ AddDerivationToCAP( MorphismFromCocartesianBidualWithGivenCocartesianBidual,
                       [ CocartesianEvaluationForCocartesianDual, 1 ],
                       [ CocartesianBraiding, 1 ],
                       [ CocartesianDualOnObjects, 2 ],
-                      [ UniversalPropertyOfCocartesianDual, 1 ] ],
+                      [ UniversalPropertyOfCocartesianDualWithGivenCocartesianDualObject, 1 ] ],
 
   function( cat, a, avv )
     local alpha;
@@ -173,7 +173,7 @@ AddDerivationToCAP( MorphismFromCocartesianBidualWithGivenCocartesianBidual,
                   CocartesianEvaluationForCocartesianDual( cat, a ),
                   CocartesianBraiding( cat, CocartesianDualOnObjects( cat, a ), a ) );
 
-    return UniversalPropertyOfCocartesianDual( cat, a, CocartesianDualOnObjects( cat, a ), alpha );
+    return UniversalPropertyOfCocartesianDualWithGivenCocartesianDualObject( cat, a, CocartesianDualOnObjects( cat, a ), alpha, avv );
 
 end : CategoryFilter := IsCocartesianCoclosedCategory );
 

CartesianCategories/gap/Tools.gi

@@ -311,6 +311,8 @@ WriteFileForClosedMonoidalStructure(
                                ## UniversalPropertyOfDual
                                [ "dual_operation := \"UniversalPropertyOfCoDual\"",
                                  "dual_operation := \"UniversalPropertyOfCocartesianDual\"" ],
+                               [ "dual_operation := \"UniversalPropertyOfCoDualWithGivenCoDualObject\"",
+                                 "dual_operation := \"UniversalPropertyOfCocartesianDualWithGivenCocartesianDualObject\"" ],
                                ##############################
                                ## Safe replacements for Tests
                                ##############################
@@ -703,6 +705,8 @@ WriteFileForCoclosedMonoidalStructure(
                                ## UniversalPropertyOfCoDual
                                [ "dual_operation := \"UniversalPropertyOfDual\"",
                                  "dual_operation := \"UniversalPropertyOfCartesianDual\"" ],
+                               [ "dual_operation := \"UniversalPropertyOfDualWithGivenDualObject\"",
+                                 "dual_operation := \"UniversalPropertyOfCartesianDualWithGivenCartesianDualObject\"" ],
                                [ "CLOSED_AND_COCLOSED_MONOIDAL_CATEGORIES",
                                  "CARTESIAN_CLOSED_AND_COCARTESIAN_COCLOSED_CATEGORIES" ],
                                [ "COCLOSED_MONOIDAL_CATEGORIES_METHOD",

MonoidalCategories/PackageInfo.g

@@ -10,7 +10,7 @@ SetPackageInfo( rec(
 
 PackageName := "MonoidalCategories",
 Subtitle := "Monoidal and monoidal (co)closed categories",
-Version := "2023.11-02",
+Version := "2023.11-03",
 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",
 

MonoidalCategories/gap/ClosedMonoidalCategories.autogen.gd

@@ -711,3 +711,22 @@ DeclareOperation( "AddUniversalPropertyOfDual",
 
 DeclareOperation( "AddUniversalPropertyOfDual",
                   [ IsCapCategory, IsList ] );
+
+#! @Description
+#! The arguments are a category $C$ and a function $F$.
+#! This operation adds the given function $F$
+#! to the category for the basic operation `UniversalPropertyOfDualWithGivenDualObject`.
+#! $F: ( t, a, alpha, d ) \mapsto \mathtt{UniversalPropertyOfDualWithGivenDualObject}(t, a, alpha, d)$.
+#! @Returns nothing
+#! @Arguments C, F
+DeclareOperation( "AddUniversalPropertyOfDualWithGivenDualObject",
+                  [ IsCapCategory, IsFunction ] );
+
+DeclareOperation( "AddUniversalPropertyOfDualWithGivenDualObject",
+                  [ IsCapCategory, IsFunction, IsInt ] );
+
+DeclareOperation( "AddUniversalPropertyOfDualWithGivenDualObject",
+                  [ IsCapCategory, IsList, IsInt ] );
+
+DeclareOperation( "AddUniversalPropertyOfDualWithGivenDualObject",
+                  [ IsCapCategory, IsList ] );

MonoidalCategories/gap/ClosedMonoidalCategories.gd

@@ -314,6 +314,17 @@ DeclareAttribute( "IsomorphismFromInternalHomIntoTensorUnitToDualObject",
 DeclareOperation( "UniversalPropertyOfDual",
                   [ IsCapCategoryObject, IsCapCategoryObject, IsCapCategoryMorphism ] );
 
+#! @Description
+#! The arguments are two objects $t,a$,
+#! a morphism $\alpha: t \otimes a \rightarrow 1$ and
+#! the dual object $d = a^{\vee}$.
+#! The output is the morphism $t \rightarrow a^{\vee}$
+#! given by the universal property of $a^{\vee}$.
+#! @Returns a morphism in $\mathrm{Hom}(t, a^{\vee})$.
+#! @Arguments t, a, alpha, d
+DeclareOperation( "UniversalPropertyOfDualWithGivenDualObject",
+                  [ IsCapCategoryObject, IsCapCategoryObject, IsCapCategoryMorphism, IsCapCategoryObject ] );
+
 #! @Description
 #! The argument is a morphism $\alpha: a \rightarrow b$.
 #! The output is the corresponding morphism $1 \rightarrow \mathrm{\underline{Hom}}(a,b)$

MonoidalCategories/gap/ClosedMonoidalCategoriesMethodRecord.gi

@@ -400,6 +400,18 @@ UniversalPropertyOfDual := rec(
   # Test in ClosedMonoidalCategoriesTest
 ),
 
+UniversalPropertyOfDualWithGivenDualObject:= rec(
+  filter_list := [ "category", "object", "object", "morphism", "object" ],
+  input_arguments_names := [ "cat", "t", "a", "alpha", "d" ],
+  output_source_getter_string := "t",
+  output_source_getter_preconditions := [ ],
+  output_range_getter_string := "d",
+  output_range_getter_preconditions := [ ],
+  return_type := "morphism",
+  dual_operation := "UniversalPropertyOfCoDualWithGivenCoDualObject",
+  dual_arguments_reversed := false,
+),
+
 LambdaIntroduction := rec(
   filter_list := [ "category", "morphism" ],
   return_type := "morphism",

MonoidalCategories/gap/CoclosedMonoidalCategories.autogen.gd

@@ -711,3 +711,22 @@ DeclareOperation( "AddUniversalPropertyOfCoDual",
 
 DeclareOperation( "AddUniversalPropertyOfCoDual",
                   [ IsCapCategory, IsList ] );
+
+#! @Description
+#! The arguments are a category $C$ and a function $F$.
+#! This operation adds the given function $F$
+#! to the category for the basic operation `UniversalPropertyOfCoDualWithGivenCoDualObject`.
+#! $F: ( t, a, alpha, c ) \mapsto \mathtt{UniversalPropertyOfCoDualWithGivenCoDualObject}(t, a, alpha, c)$.
+#! @Returns nothing
+#! @Arguments C, F
+DeclareOperation( "AddUniversalPropertyOfCoDualWithGivenCoDualObject",
+                  [ IsCapCategory, IsFunction ] );
+
+DeclareOperation( "AddUniversalPropertyOfCoDualWithGivenCoDualObject",
+                  [ IsCapCategory, IsFunction, IsInt ] );
+
+DeclareOperation( "AddUniversalPropertyOfCoDualWithGivenCoDualObject",
+                  [ IsCapCategory, IsList, IsInt ] );
+
+DeclareOperation( "AddUniversalPropertyOfCoDualWithGivenCoDualObject",
+                  [ IsCapCategory, IsList ] );

MonoidalCategories/gap/CoclosedMonoidalCategories.gd

@@ -311,6 +311,17 @@ DeclareAttribute( "IsomorphismFromInternalCoHomFromTensorUnitToCoDualObject",
 DeclareOperation( "UniversalPropertyOfCoDual",
                   [ IsCapCategoryObject, IsCapCategoryObject, IsCapCategoryMorphism ] );
 
+#! @Description
+#! The arguments are two objects $t,a$,
+#! a morphism $\alpha: 1 \rightarrow t \otimes a$ and
+#! the codual object $c = a_{\vee}$.
+#! The output is the morphism $a_{\vee} \rightarrow t$
+#! given by the universal property of $a_{\vee}$.
+#! @Returns a morphism in $\mathrm{Hom}(a_{\vee}, t)$.
+#! @Arguments t, a, alpha, c
+DeclareOperation( "UniversalPropertyOfCoDualWithGivenCoDualObject",
+                  [ IsCapCategoryObject, IsCapCategoryObject, IsCapCategoryMorphism, IsCapCategoryObject] );
+
 #! @Description
 #! The argument is a morphism $\alpha: a \rightarrow b$.
 #! The output is the corresponding morphism $ \mathrm{\underline{coHom}}(a,b) \rightarrow 1$

MonoidalCategories/gap/CoclosedMonoidalCategoriesMethodRecord.gi

@@ -400,6 +400,18 @@ UniversalPropertyOfCoDual := rec(
   # Test in CoclosedMonoidalCategoriesTest
 ),
 
+UniversalPropertyOfCoDualWithGivenCoDualObject := rec(
+  filter_list := [ "category", "object", "object", "morphism", "object" ],
+  input_arguments_names := [ "cat", "t", "a", "alpha", "c" ],
+  output_source_getter_string := "c",
+  output_source_getter_preconditions := [ ],
+  output_range_getter_string := "t",
+  output_range_getter_preconditions := [ ],
+  return_type := "morphism",
+  dual_operation := "UniversalPropertyOfDualWithGivenDualObject",
+  dual_arguments_reversed := false,
+),
+
 CoLambdaIntroduction := rec(
   filter_list := [ "category", "morphism" ],
   return_type := "morphism",

MonoidalCategories/gap/SymmetricClosedMonoidalCategoriesDerivedMethods.gi

@@ -148,7 +148,7 @@ AddDerivationToCAP( MorphismToBidualWithGivenBidual,
                       [ Braiding, 1 ],
                       [ DualOnObjects, 2 ],
                       [ EvaluationForDual, 1 ],
-                      [ UniversalPropertyOfDual, 1 ] ],
+                      [ UniversalPropertyOfDualWithGivenDualObject, 1 ] ],
 
   function( cat, a, avv )
     local alpha;
@@ -168,7 +168,7 @@ AddDerivationToCAP( MorphismToBidualWithGivenBidual,
     alpha := PreCompose( cat, Braiding( cat, a, DualOnObjects( cat, a ) ),
                             EvaluationForDual( cat, a ) );
 
-    return UniversalPropertyOfDual( cat, a, DualOnObjects( cat, a ), alpha );
+    return UniversalPropertyOfDualWithGivenDualObject( cat, a, DualOnObjects( cat, a ), alpha, avv );
 
 end : CategoryFilter := IsSymmetricClosedMonoidalCategory );
 

MonoidalCategories/gap/SymmetricCoclosedMonoidalCategoriesDerivedMethods.gi

@@ -148,7 +148,7 @@ AddDerivationToCAP( MorphismFromCoBidualWithGivenCoBidual,
                       [ CoclosedEvaluationForCoDual, 1 ],
                       [ Braiding, 1 ],
                       [ CoDualOnObjects, 2 ],
-                      [ UniversalPropertyOfCoDual, 1 ] ],
+                      [ UniversalPropertyOfCoDualWithGivenCoDualObject, 1 ] ],
 
   function( cat, a, avv )
     local alpha;
@@ -170,7 +170,7 @@ AddDerivationToCAP( MorphismFromCoBidualWithGivenCoBidual,
                   CoclosedEvaluationForCoDual( cat, a ),
                   Braiding( cat, CoDualOnObjects( cat, a ), a ) );
 
-    return UniversalPropertyOfCoDual( cat, a, CoDualOnObjects( cat, a ), alpha );
+    return UniversalPropertyOfCoDualWithGivenCoDualObject( cat, a, CoDualOnObjects( cat, a ), alpha, avv );
 
 end : CategoryFilter := IsSymmetricCoclosedMonoidalCategory );