Regenerate CartesianCategories

* from MonoidalCategories v2023.10-01

Author: Tom Kuhmichel

CartesianCategories/PackageInfo.g

@@ -10,7 +10,7 @@ SetPackageInfo( rec(
 
 PackageName := "CartesianCategories",
 Subtitle := "Cartesian and cocartesian categories and various subdoctrines",
-Version := "2023.08-14",
+Version := "2023.10-01",
 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.08-11
+* from MonoidalCategories v2023.10-01

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

@@ -397,6 +397,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" ],
   input_arguments_names := [ "cat", "alpha" ],

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

@@ -397,6 +397,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" ],
   input_arguments_names := [ "cat", "alpha" ],

CartesianCategories/gap/SymmetricCartesianClosedCategoriesDerivedMethods.gi

@@ -120,7 +120,7 @@ AddDerivationToCAP( MorphismToCartesianBidualWithGivenCartesianBidual,
                       [ CartesianBraiding, 1 ],
                       [ CartesianDualOnObjects, 2 ],
                       [ CartesianEvaluationForCartesianDual, 1 ],
-                      [ UniversalPropertyOfCartesianDual, 1 ] ],
+                      [ UniversalPropertyOfCartesianDualWithGivenCartesianDualObject, 1 ] ],
 
   function( cat, a, avv )
     local alpha;
@@ -140,7 +140,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

@@ -120,7 +120,7 @@ AddDerivationToCAP( MorphismFromCocartesianBidualWithGivenCocartesianBidual,
                       [ CocartesianEvaluationForCocartesianDual, 1 ],
                       [ CocartesianBraiding, 1 ],
                       [ CocartesianDualOnObjects, 2 ],
-                      [ UniversalPropertyOfCocartesianDual, 1 ] ],
+                      [ UniversalPropertyOfCocartesianDualWithGivenCocartesianDualObject, 1 ] ],
 
   function( cat, a, avv )
     local alpha;
@@ -142,7 +142,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 );