From 5377eefbcb969e6961517d0f4ea748891a7b269e Mon Sep 17 00:00:00 2001 From: Tom Kuhmichel Date: Fri, 6 Oct 2023 18:44:00 +0200 Subject: [PATCH] Regenerate CartesianCategories * from MonoidalCategories v2023.10-01 --- CartesianCategories/PackageInfo.g | 2 +- CartesianCategories/gap/AUTOGENERATED_FROM.md | 2 +- .../gap/CartesianClosedCategories.autogen.gd | 19 +++++++++++++++++++ .../gap/CartesianClosedCategories.gd | 11 +++++++++++ .../CartesianClosedCategoriesMethodRecord.gi | 12 ++++++++++++ .../CocartesianCoclosedCategories.autogen.gd | 19 +++++++++++++++++++ .../gap/CocartesianCoclosedCategories.gd | 11 +++++++++++ ...cartesianCoclosedCategoriesMethodRecord.gi | 12 ++++++++++++ ...CartesianClosedCategoriesDerivedMethods.gi | 4 ++-- ...rtesianCoclosedCategoriesDerivedMethods.gi | 4 ++-- CartesianCategories/gap/Tools.gi | 4 ++++ 11 files changed, 94 insertions(+), 6 deletions(-) diff --git a/CartesianCategories/PackageInfo.g b/CartesianCategories/PackageInfo.g index ec089791d6..db0b4b6cbd 100644 --- a/CartesianCategories/PackageInfo.g +++ b/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", diff --git a/CartesianCategories/gap/AUTOGENERATED_FROM.md b/CartesianCategories/gap/AUTOGENERATED_FROM.md index 8f1856d6cd..611b623b4f 100644 --- a/CartesianCategories/gap/AUTOGENERATED_FROM.md +++ b/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 diff --git a/CartesianCategories/gap/CartesianClosedCategories.autogen.gd b/CartesianCategories/gap/CartesianClosedCategories.autogen.gd index e48aeb0a91..e287bad9a0 100644 --- a/CartesianCategories/gap/CartesianClosedCategories.autogen.gd +++ b/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 ] ); diff --git a/CartesianCategories/gap/CartesianClosedCategories.gd b/CartesianCategories/gap/CartesianClosedCategories.gd index 24a74d3af7..902308bfdd 100644 --- a/CartesianCategories/gap/CartesianClosedCategories.gd +++ b/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)$ diff --git a/CartesianCategories/gap/CartesianClosedCategoriesMethodRecord.gi b/CartesianCategories/gap/CartesianClosedCategoriesMethodRecord.gi index e1e081b70a..5e68da2175 100644 --- a/CartesianCategories/gap/CartesianClosedCategoriesMethodRecord.gi +++ 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", diff --git a/CartesianCategories/gap/CocartesianCoclosedCategories.autogen.gd b/CartesianCategories/gap/CocartesianCoclosedCategories.autogen.gd index ac3387bf7a..7f67c4f872 100644 --- a/CartesianCategories/gap/CocartesianCoclosedCategories.autogen.gd +++ b/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 ] ); diff --git a/CartesianCategories/gap/CocartesianCoclosedCategories.gd b/CartesianCategories/gap/CocartesianCoclosedCategories.gd index 784b965386..3356946531 100644 --- a/CartesianCategories/gap/CocartesianCoclosedCategories.gd +++ b/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$ diff --git a/CartesianCategories/gap/CocartesianCoclosedCategoriesMethodRecord.gi b/CartesianCategories/gap/CocartesianCoclosedCategoriesMethodRecord.gi index aa1acd9ae8..9a10c6d4be 100644 --- a/CartesianCategories/gap/CocartesianCoclosedCategoriesMethodRecord.gi +++ b/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", diff --git a/CartesianCategories/gap/SymmetricCartesianClosedCategoriesDerivedMethods.gi b/CartesianCategories/gap/SymmetricCartesianClosedCategoriesDerivedMethods.gi index 97914446f6..14278ce252 100644 --- a/CartesianCategories/gap/SymmetricCartesianClosedCategoriesDerivedMethods.gi +++ b/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 ); diff --git a/CartesianCategories/gap/SymmetricCocartesianCoclosedCategoriesDerivedMethods.gi b/CartesianCategories/gap/SymmetricCocartesianCoclosedCategoriesDerivedMethods.gi index d7b171053c..95b9fc9813 100644 --- a/CartesianCategories/gap/SymmetricCocartesianCoclosedCategoriesDerivedMethods.gi +++ b/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 ); diff --git a/CartesianCategories/gap/Tools.gi b/CartesianCategories/gap/Tools.gi index 7686e456ff..4fb131b439 100644 --- a/CartesianCategories/gap/Tools.gi +++ b/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",