From 04b757cfd4280bc1d11b0b681f4cc2697fb3fe57 Mon Sep 17 00:00:00 2001 From: Fabian Zickgraf Date: Mon, 31 Jul 2023 14:57:38 +0200 Subject: [PATCH] Replace io_types by input_arguments_names etc. --- CAP/PackageInfo.g | 2 +- CAP/gap/LimitConvenience.gi | 28 +- CAP/gap/MethodRecord.gi | 980 +++++++++++++----- CartesianCategories/PackageInfo.g | 2 +- .../BraidedCartesianCategoriesMethodRecord.gi | 16 +- ...raidedCocartesianCategoriesMethodRecord.gi | 16 +- .../gap/CartesianCategoriesMethodRecord.gi | 72 +- .../CartesianClosedCategoriesMethodRecord.gi | 142 ++- .../gap/CocartesianCategoriesMethodRecord.gi | 72 +- ...cartesianCoclosedCategoriesMethodRecord.gi | 142 ++- ...butiveCocartesianCategoriesMethodRecord.gi | 32 +- ...ributiveCartesianCategoriesMethodRecord.gi | 32 +- FreydCategoriesForCAP/PackageInfo.g | 2 +- .../gap/FreydCategoriesForCAP.gi | 144 ++- MonoidalCategories/PackageInfo.g | 2 +- .../AdditiveMonoidalCategoriesMethodRecord.gi | 32 +- .../BraidedMonoidalCategoriesMethodRecord.gi | 16 +- .../ClosedMonoidalCategoriesMethodRecord.gi | 142 ++- .../CoclosedMonoidalCategoriesMethodRecord.gi | 142 ++- .../gap/MonoidalCategoriesMethodRecord.gi | 64 +- ...ricClosedMonoidalCategoriesMethodRecord.gi | 34 +- ...cCoclosedMonoidalCategoriesMethodRecord.gi | 34 +- 22 files changed, 1627 insertions(+), 521 deletions(-) diff --git a/CAP/PackageInfo.g b/CAP/PackageInfo.g index 260781566a..6d067e1723 100644 --- a/CAP/PackageInfo.g +++ b/CAP/PackageInfo.g @@ -10,7 +10,7 @@ SetPackageInfo( rec( PackageName := "CAP", Subtitle := "Categories, Algorithms, Programming", -Version := "2023.07-08", +Version := "2023.07-09", 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/CAP/gap/LimitConvenience.gi b/CAP/gap/LimitConvenience.gi index bce21fc1d4..1ca7631c0a 100644 --- a/CAP/gap/LimitConvenience.gi +++ b/CAP/gap/LimitConvenience.gi @@ -6,7 +6,7 @@ InstallGlobalFunction( "CAP_INTERNAL_GENERATE_CONVENIENCE_METHODS_FOR_LIMITS", function ( package_name, method_name_record, limits ) - local output_string, generate_universal_morphism_convenience, generate_functorial_convenience_method, number_of_diagram_arguments, functorial_record, filter_list, input_type, replaced_filter_list, arguments_string, source_diagram_arguments_string, range_diagram_arguments_string, source_diagram_input_type, range_diagram_input_type, limit, output_path; + local output_string, generate_universal_morphism_convenience, generate_functorial_convenience_method, number_of_diagram_arguments, limit, output_path; output_string := """# SPDX-License-Identifier: GPL-2.0-or-later @@ -165,7 +165,7 @@ end ); with_given_universal_morphism := Concatenation( universal_morphism_name, "WithGiven", object_name ), diagram_filter_list := List( CAP_INTERNAL_REPLACED_STRINGS_WITH_FILTERS( limit.diagram_filter_list ), NameFunction ), tau_filter := tau_filter, - diagram_arguments := limit.diagram_input_type, + diagram_arguments := limit.diagram_arguments_names, test_object_position := test_object_position, selected_tau := Concatenation( "tau", list_selector ), ) @@ -178,7 +178,7 @@ end ); end; generate_functorial_convenience_method := function( limit, limit_colimit, object_name, functorial_name, functorial_with_given_name ) - local functorial_with_given_record, filter_list, input_type, arguments_string, source_diagram_arguments_string, range_diagram_arguments_string, replaced_filter_list, current_string, input_arguments_names, source_argument_name, range_argument_name, source_diagram_arguments_names, range_diagram_arguments_names, equalizer_preprocessing, test_string, additional_preconditions, test_arguments, universal_morphism_with_given_name, call_arguments; + local functorial_with_given_record, filter_list, arguments_names, arguments_string, source_diagram_arguments_string, range_diagram_arguments_string, replaced_filter_list, current_string, input_arguments_names, source_argument_name, range_argument_name, source_diagram_arguments_names, range_diagram_arguments_names, equalizer_preprocessing, test_string, additional_preconditions, test_arguments, universal_morphism_with_given_name, call_arguments; Assert( 0, limit_colimit in [ "limit", "colimit" ] ); @@ -188,12 +188,12 @@ end ); # convenience: derive diagrams from arguments filter_list := limit.diagram_morphism_filter_list; - input_type := limit.diagram_morphism_input_type; + arguments_names := limit.diagram_morphism_arguments_names; Assert( 0, Length( filter_list ) = 1 ); - Assert( 0, Length( input_type ) = 1 ); + Assert( 0, Length( arguments_names ) = 1 ); - arguments_string := JoinStringsWithSeparator( input_type, ", " ); + arguments_string := JoinStringsWithSeparator( arguments_names, ", " ); if limit.number_of_targets = 1 then source_diagram_arguments_string := Concatenation( "Source( ", arguments_string, " )" ); @@ -219,7 +219,7 @@ end ); rec( functorial_name := functorial_name, filter_list := replaced_filter_list, - input_arguments := input_type, + input_arguments := arguments_names, source_diagram_arguments := source_diagram_arguments_string, range_diagram_arguments := range_diagram_arguments_string, ) @@ -242,7 +242,7 @@ end ); rec( functorial_name := functorial_name, filter_list := replaced_filter_list, - input_arguments := input_type, + input_arguments := arguments_names, source_diagram_arguments := source_diagram_arguments_string, range_diagram_arguments := range_diagram_arguments_string, ) @@ -264,7 +264,7 @@ end ); rec( functorial_with_given_name := functorial_with_given_name, filter_list := replaced_filter_list, - input_arguments := input_type, + input_arguments := arguments_names, source_diagram_arguments := source_diagram_arguments_string, range_diagram_arguments := range_diagram_arguments_string, ) @@ -287,7 +287,7 @@ end ); rec( functorial_with_given_name := functorial_with_given_name, filter_list := replaced_filter_list, - input_arguments := input_type, + input_arguments := arguments_names, source_diagram_arguments := source_diagram_arguments_string, range_diagram_arguments := range_diagram_arguments_string, ) @@ -299,7 +299,7 @@ end ); # derive functorials from the universality of the limit/colimit Assert( 0, Length( limit.diagram_morphism_filter_list ) <= 1 ); - Assert( 0, Length( limit.diagram_morphism_input_type ) <= 1 ); + Assert( 0, Length( limit.diagram_morphism_arguments_names ) <= 1 ); input_arguments_names := functorial_with_given_record.input_arguments_names; @@ -317,7 +317,7 @@ end ); if limit.number_of_targets = 1 then - Assert( 0, limit.diagram_morphism_input_type = [ "mu" ] ); + Assert( 0, limit.diagram_morphism_arguments_names = [ "mu" ] ); if limit_colimit = "limit" then @@ -366,7 +366,7 @@ end ); else - Assert( 0, limit.diagram_morphism_input_type = [ "L" ] ); + Assert( 0, limit.diagram_morphism_arguments_names = [ "L" ] ); if limit_colimit = "limit" then @@ -406,7 +406,7 @@ end ); else - Assert( 0, limit.diagram_morphism_input_type = [ ] ); + Assert( 0, limit.diagram_morphism_arguments_names = [ ] ); test_arguments := [ ]; diff --git a/CAP/gap/MethodRecord.gi b/CAP/gap/MethodRecord.gi index d6f2312c3e..08396c239a 100644 --- a/CAP/gap/MethodRecord.gi +++ b/CAP/gap/MethodRecord.gi @@ -107,7 +107,11 @@ MorphismDatum := rec( LiftAlongMonomorphism := rec( filter_list := [ "category", "morphism", "morphism" ], - io_type := [ [ "iota", "tau" ], [ "tau_source", "iota_source" ] ], + input_arguments_names := [ "cat", "iota", "tau" ], + output_source_getter_string := "Source( tau )", + output_source_getter_preconditions := [ ], + output_range_getter_string := "Source( iota )", + output_range_getter_preconditions := [ ], pre_function := function( cat, iota, tau ) if not IsEqualForObjects( cat, Range( iota ), Range( tau ) ) then @@ -142,7 +146,11 @@ IsLiftableAlongMonomorphism := rec( ColiftAlongEpimorphism := rec( filter_list := [ "category", "morphism", "morphism" ], - io_type := [ [ "epsilon", "tau" ], [ "epsilon_range", "tau_range" ] ], + input_arguments_names := [ "cat", "epsilon", "tau" ], + output_source_getter_string := "Range( epsilon )", + output_source_getter_preconditions := [ ], + output_range_getter_string := "Range( tau )", + output_range_getter_preconditions := [ ], pre_function := function( cat, epsilon, tau ) if not IsEqualForObjects( cat, Source( epsilon ), Source( tau ) ) then @@ -177,7 +185,11 @@ IsColiftableAlongEpimorphism := rec( Lift := rec( filter_list := [ "category", "morphism", "morphism" ], - io_type := [ [ "alpha", "beta" ], [ "alpha_source", "beta_source" ] ], + input_arguments_names := [ "cat", "alpha", "beta" ], + output_source_getter_string := "Source( alpha )", + output_source_getter_preconditions := [ ], + output_range_getter_string := "Source( beta )", + output_range_getter_preconditions := [ ], pre_function := function( cat, iota, tau ) if not IsEqualForObjects( cat, Range( iota ), Range( tau ) ) then @@ -197,7 +209,11 @@ Lift := rec( LiftOrFail := rec( filter_list := [ "category", "morphism", "morphism" ], - io_type := [ [ "alpha", "beta" ], [ "alpha_source", "beta_source" ] ], + input_arguments_names := [ "cat", "alpha", "beta" ], + output_source_getter_string := "Source( alpha )", + output_source_getter_preconditions := [ ], + output_range_getter_string := "Source( beta )", + output_range_getter_preconditions := [ ], pre_function := "Lift", return_type := "morphism_or_fail", dual_operation := "ColiftOrFail", @@ -217,7 +233,11 @@ IsLiftable := rec( Colift := rec( filter_list := [ "category", "morphism", "morphism" ], - io_type := [ [ "alpha", "beta" ], [ "alpha_range", "beta_range" ] ], + input_arguments_names := [ "cat", "alpha", "beta" ], + output_source_getter_string := "Range( alpha )", + output_source_getter_preconditions := [ ], + output_range_getter_string := "Range( beta )", + output_range_getter_preconditions := [ ], pre_function := function( cat, epsilon, tau ) if not IsEqualForObjects( cat, Source( epsilon ), Source( tau ) ) then @@ -237,7 +257,11 @@ Colift := rec( ColiftOrFail := rec( filter_list := [ "category", "morphism", "morphism" ], - io_type := [ [ "alpha", "beta" ], [ "alpha_range", "beta_range" ] ], + input_arguments_names := [ "cat", "alpha", "beta" ], + output_source_getter_string := "Range( alpha )", + output_source_getter_preconditions := [ ], + output_range_getter_string := "Range( beta )", + output_range_getter_preconditions := [ ], pre_function := "Colift", return_type := "morphism_or_fail", dual_operation := "LiftOrFail", @@ -257,7 +281,11 @@ IsColiftable := rec( ProjectiveLift := rec( filter_list := [ "category", "morphism", "morphism" ], - io_type := [ [ "alpha", "beta" ], [ "alpha_source", "beta_source" ] ], + input_arguments_names := [ "cat", "alpha", "beta" ], + output_source_getter_string := "Source( alpha )", + output_source_getter_preconditions := [ ], + output_range_getter_string := "Source( beta )", + output_range_getter_preconditions := [ ], pre_function := function( cat, iota, tau ) if not IsEqualForObjects( cat, Range( iota ), Range( tau ) ) then @@ -276,7 +304,11 @@ ProjectiveLift := rec( InjectiveColift := rec( filter_list := [ "category", "morphism", "morphism" ], - io_type := [ [ "alpha", "beta" ], [ "alpha_range", "beta_range" ] ], + input_arguments_names := [ "cat", "alpha", "beta" ], + output_source_getter_string := "Range( alpha )", + output_source_getter_preconditions := [ ], + output_range_getter_string := "Range( beta )", + output_range_getter_preconditions := [ ], pre_function := function( cat, epsilon, tau ) if not IsEqualForObjects( cat, Source( epsilon ), Source( tau ) ) then @@ -295,14 +327,22 @@ InjectiveColift := rec( IdentityMorphism := rec( filter_list := [ "category", "object" ], - io_type := [ [ "a" ], [ "a", "a" ] ], + input_arguments_names := [ "cat", "a" ], + output_source_getter_string := "a", + output_source_getter_preconditions := [ ], + output_range_getter_string := "a", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "IdentityMorphism" ), InverseForMorphisms := rec( # Type check for IsIsomorphism filter_list := [ "category", "morphism" ], - io_type := [ [ "alpha" ], [ "alpha_range", "alpha_source" ] ], + input_arguments_names := [ "cat", "alpha" ], + output_source_getter_string := "Range( alpha )", + output_source_getter_preconditions := [ ], + output_range_getter_string := "Source( alpha )", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "InverseForMorphisms", compatible_with_congruence_of_morphisms := true, @@ -310,7 +350,11 @@ InverseForMorphisms := rec( PreInverseForMorphisms := rec( filter_list := [ "category", "morphism" ], - io_type := [ [ "alpha" ], [ "alpha_range", "alpha_source" ] ], + input_arguments_names := [ "cat", "alpha" ], + output_source_getter_string := "Range( alpha )", + output_source_getter_preconditions := [ ], + output_range_getter_string := "Source( alpha )", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "PostInverseForMorphisms", is_merely_set_theoretic := true @@ -318,7 +362,11 @@ PreInverseForMorphisms := rec( PostInverseForMorphisms := rec( filter_list := [ "category", "morphism" ], - io_type := [ [ "alpha" ], [ "alpha_range", "alpha_source" ] ], + input_arguments_names := [ "cat", "alpha" ], + output_source_getter_string := "Range( alpha )", + output_source_getter_preconditions := [ ], + output_range_getter_string := "Source( alpha )", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "PreInverseForMorphisms", is_merely_set_theoretic := true @@ -335,7 +383,9 @@ KernelObject := rec( KernelEmbedding := rec( filter_list := [ "category", "morphism" ], - io_type := [ [ "alpha" ], [ "P", "alpha_source" ] ], + input_arguments_names := [ "cat", "alpha" ], + output_range_getter_string := "Source( alpha )", + output_range_getter_preconditions := [ ], with_given_object_position := "Source", return_type := "morphism", dual_operation := "CokernelProjection", @@ -344,7 +394,11 @@ KernelEmbedding := rec( KernelEmbeddingWithGivenKernelObject := rec( filter_list := [ "category", "morphism", "object" ], - io_type := [ [ "alpha", "P" ], [ "P", "alpha_source" ] ], + input_arguments_names := [ "cat", "alpha", "P" ], + output_source_getter_string := "P", + output_source_getter_preconditions := [ ], + output_range_getter_string := "Source( alpha )", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "CokernelProjectionWithGivenCokernelObject", compatible_with_congruence_of_morphisms := false, @@ -352,7 +406,9 @@ KernelEmbeddingWithGivenKernelObject := rec( MorphismFromKernelObjectToSink := rec( filter_list := [ "category", "morphism" ], - io_type := [ [ "alpha" ], [ "P", "alpha_range" ] ], + input_arguments_names := [ "cat", "alpha" ], + output_range_getter_string := "Range( alpha )", + output_range_getter_preconditions := [ ], with_given_object_position := "Source", dual_operation := "MorphismFromSourceToCokernelObject", return_type := "morphism", @@ -361,7 +417,11 @@ MorphismFromKernelObjectToSink := rec( MorphismFromKernelObjectToSinkWithGivenKernelObject := rec( filter_list := [ "category", "morphism", "object" ], - io_type := [ [ "alpha", "P" ], [ "P", "alpha_range" ] ], + input_arguments_names := [ "cat", "alpha", "P" ], + output_source_getter_string := "P", + output_source_getter_preconditions := [ ], + output_range_getter_string := "Range( alpha )", + output_range_getter_preconditions := [ ], dual_operation := "MorphismFromSourceToCokernelObjectWithGivenCokernelObject", return_type := "morphism", compatible_with_congruence_of_morphisms := false, @@ -369,7 +429,9 @@ MorphismFromKernelObjectToSinkWithGivenKernelObject := rec( KernelLift := rec( filter_list := [ "category", "morphism", "object", "morphism" ], - io_type := [ [ "alpha", "T", "tau" ], [ "T", "P" ] ], + input_arguments_names := [ "cat", "alpha", "T", "tau" ], + output_source_getter_string := "T", + output_source_getter_preconditions := [ ], with_given_object_position := "Range", return_type := "morphism", dual_operation := "CokernelColift", @@ -378,7 +440,11 @@ KernelLift := rec( KernelLiftWithGivenKernelObject := rec( filter_list := [ "category", "morphism", "object", "morphism", "object" ], - io_type := [ [ "alpha", "T", "tau", "P" ], [ "T", "P" ] ], + input_arguments_names := [ "cat", "alpha", "T", "tau", "P" ], + output_source_getter_string := "T", + output_source_getter_preconditions := [ ], + output_range_getter_string := "P", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "CokernelColiftWithGivenCokernelObject", compatible_with_congruence_of_morphisms := false, @@ -395,7 +461,9 @@ CokernelObject := rec( CokernelProjection := rec( filter_list := [ "category", "morphism" ], - io_type := [ [ "alpha" ], [ "alpha_range", "P" ] ], + input_arguments_names := [ "cat", "alpha" ], + output_source_getter_string := "Range( alpha )", + output_source_getter_preconditions := [ ], with_given_object_position := "Range", return_type := "morphism", dual_operation := "KernelEmbedding", @@ -404,7 +472,11 @@ CokernelProjection := rec( CokernelProjectionWithGivenCokernelObject := rec( filter_list := [ "category", "morphism", "object" ], - io_type := [ [ "alpha", "P" ], [ "alpha_range", "P" ] ], + input_arguments_names := [ "cat", "alpha", "P" ], + output_source_getter_string := "Range( alpha )", + output_source_getter_preconditions := [ ], + output_range_getter_string := "P", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "KernelEmbeddingWithGivenKernelObject", compatible_with_congruence_of_morphisms := false, @@ -412,7 +484,9 @@ CokernelProjectionWithGivenCokernelObject := rec( MorphismFromSourceToCokernelObject := rec( filter_list := [ "category", "morphism" ], - io_type := [ [ "alpha" ], [ "alpha_source", "P" ] ], + input_arguments_names := [ "cat", "alpha" ], + output_source_getter_string := "Source( alpha )", + output_source_getter_preconditions := [ ], with_given_object_position := "Range", dual_operation := "MorphismFromKernelObjectToSink", return_type := "morphism", @@ -421,7 +495,11 @@ MorphismFromSourceToCokernelObject := rec( MorphismFromSourceToCokernelObjectWithGivenCokernelObject := rec( filter_list := [ "category", "morphism", "object" ], - io_type := [ [ "alpha", "P" ], [ "alpha_source", "P" ] ], + input_arguments_names := [ "cat", "alpha", "P" ], + output_source_getter_string := "Source( alpha )", + output_source_getter_preconditions := [ ], + output_range_getter_string := "P", + output_range_getter_preconditions := [ ], dual_operation := "MorphismFromKernelObjectToSinkWithGivenKernelObject", return_type := "morphism", compatible_with_congruence_of_morphisms := false, @@ -429,7 +507,9 @@ MorphismFromSourceToCokernelObjectWithGivenCokernelObject := rec( CokernelColift := rec( filter_list := [ "category", "morphism", "object", "morphism" ], - io_type := [ [ "alpha", "T", "tau" ], [ "P", "T" ] ], + input_arguments_names := [ "cat", "alpha", "T", "tau" ], + output_range_getter_string := "T", + output_range_getter_preconditions := [ ], with_given_object_position := "Source", return_type := "morphism", dual_operation := "KernelLift", @@ -438,7 +518,11 @@ CokernelColift := rec( CokernelColiftWithGivenCokernelObject := rec( filter_list := [ "category", "morphism", "object", "morphism", "object" ], - io_type := [ [ "alpha", "T", "tau", "P" ], [ "P", "T" ] ], + input_arguments_names := [ "cat", "alpha", "T", "tau", "P" ], + output_source_getter_string := "P", + output_source_getter_preconditions := [ ], + output_range_getter_string := "T", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "KernelLiftWithGivenKernelObject", compatible_with_congruence_of_morphisms := false, @@ -446,7 +530,11 @@ CokernelColiftWithGivenCokernelObject := rec( PreCompose := rec( filter_list := [ "category", "morphism", "morphism" ], - io_type := [ [ "alpha", "beta" ], [ "alpha_source", "beta_range" ] ], + input_arguments_names := [ "cat", "alpha", "beta" ], + output_source_getter_string := "Source( alpha )", + output_source_getter_preconditions := [ ], + output_range_getter_string := "Range( beta )", + output_range_getter_preconditions := [ ], pre_function := function( cat, mor_left, mor_right ) @@ -526,7 +614,11 @@ PreComposeList := rec( PostCompose := rec( filter_list := [ "category", "morphism", "morphism" ], - io_type := [ [ "beta", "alpha" ], [ "alpha_source", "beta_range" ] ], + input_arguments_names := [ "cat", "beta", "alpha" ], + output_source_getter_string := "Source( alpha )", + output_source_getter_preconditions := [ ], + output_range_getter_string := "Range( beta )", + output_range_getter_preconditions := [ ], pre_function := function( cat, mor_right, mor_left ) @@ -601,7 +693,11 @@ ZeroObjectFunctorial := rec( ZeroObjectFunctorialWithGivenZeroObjects := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "P", "Pp" ], [ "P", "Pp" ] ], + input_arguments_names := [ "cat", "P", "Pp" ], + output_source_getter_string := "P", + output_source_getter_preconditions := [ ], + output_range_getter_string := "Pp", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "ZeroObjectFunctorialWithGivenZeroObjects", dual_arguments_reversed := true @@ -609,61 +705,73 @@ ZeroObjectFunctorialWithGivenZeroObjects := rec( UniversalMorphismFromZeroObject := rec( filter_list := [ "category", "object" ], - io_type := [ [ "T" ], [ "P", "T" ] ], + input_arguments_names := [ "cat", "T" ], + output_range_getter_string := "T", + output_range_getter_preconditions := [ ], with_given_object_position := "Source", return_type := "morphism", dual_operation := "UniversalMorphismIntoZeroObject" ), UniversalMorphismFromZeroObjectWithGivenZeroObject := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "T", "P" ], [ "P", "T" ] ], + input_arguments_names := [ "cat", "T", "P" ], + output_source_getter_string := "P", + output_source_getter_preconditions := [ ], + output_range_getter_string := "T", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "UniversalMorphismIntoZeroObjectWithGivenZeroObject" ), UniversalMorphismIntoZeroObject := rec( filter_list := [ "category", "object" ], - io_type := [ [ "T" ], [ "T", "P" ] ], + input_arguments_names := [ "cat", "T" ], + output_source_getter_string := "T", + output_source_getter_preconditions := [ ], with_given_object_position := "Range", return_type := "morphism", dual_operation := "UniversalMorphismFromZeroObject" ), UniversalMorphismIntoZeroObjectWithGivenZeroObject := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "T", "P" ], [ "T", "P" ] ], + input_arguments_names := [ "cat", "T", "P" ], + output_source_getter_string := "T", + output_source_getter_preconditions := [ ], + output_range_getter_string := "P", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "UniversalMorphismFromZeroObjectWithGivenZeroObject" ), IsomorphismFromZeroObjectToInitialObject := rec( filter_list := [ "category" ], - ## TODO: io_type? return_type := "morphism", dual_operation := "IsomorphismFromTerminalObjectToZeroObject", ), IsomorphismFromInitialObjectToZeroObject := rec( filter_list := [ "category" ], - ## TODO: io_type? return_type := "morphism", dual_operation := "IsomorphismFromZeroObjectToTerminalObject", ), IsomorphismFromZeroObjectToTerminalObject := rec( filter_list := [ "category" ], - ## TODO: io_type? return_type := "morphism", dual_operation := "IsomorphismFromInitialObjectToZeroObject", ), IsomorphismFromTerminalObjectToZeroObject := rec( filter_list := [ "category" ], - ## TODO: io_type? return_type := "morphism", dual_operation := "IsomorphismFromZeroObjectToInitialObject", ), ZeroMorphism := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "a", "b" ], [ "a", "b" ] ], + input_arguments_names := [ "cat", "a", "b" ], + output_source_getter_string := "a", + output_source_getter_preconditions := [ ], + output_range_getter_string := "b", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_arguments_reversed := true, dual_operation := "ZeroMorphism" ), @@ -678,20 +786,28 @@ DirectSum := rec( ProjectionInFactorOfDirectSum := rec( filter_list := [ "category", "list_of_objects", "integer" ], - io_type := [ [ "objects", "k" ], [ "P", "objects_k" ] ], + input_arguments_names := [ "cat", "objects", "k" ], + output_range_getter_string := "objects[k]", + output_range_getter_preconditions := [ ], with_given_object_position := "Source", return_type := "morphism", dual_operation := "InjectionOfCofactorOfDirectSum" ), ProjectionInFactorOfDirectSumWithGivenDirectSum := rec( filter_list := [ "category", "list_of_objects", "integer", "object" ], - io_type := [ [ "objects", "k", "P" ], [ "P", "objects_k" ] ], + input_arguments_names := [ "cat", "objects", "k", "P" ], + output_source_getter_string := "P", + output_source_getter_preconditions := [ ], + output_range_getter_string := "objects[k]", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "InjectionOfCofactorOfDirectSumWithGivenDirectSum" ), UniversalMorphismIntoDirectSum := rec( filter_list := [ "category", "list_of_objects", "object", "list_of_morphisms" ], - io_type := [ [ "objects", "T", "tau" ], [ "T", "P" ] ], + input_arguments_names := [ "cat", "objects", "T", "tau" ], + output_source_getter_string := "T", + output_source_getter_preconditions := [ ], with_given_object_position := "Range", dual_operation := "UniversalMorphismFromDirectSum", @@ -717,7 +833,11 @@ UniversalMorphismIntoDirectSum := rec( UniversalMorphismIntoDirectSumWithGivenDirectSum := rec( filter_list := [ "category", "list_of_objects", "object", "list_of_morphisms", "object" ], - io_type := [ [ "objects", "T", "tau", "P" ], [ "T", "P" ] ], + input_arguments_names := [ "cat", "objects", "T", "tau", "P" ], + output_source_getter_string := "T", + output_source_getter_preconditions := [ ], + output_range_getter_string := "P", + output_range_getter_preconditions := [ ], dual_operation := "UniversalMorphismFromDirectSumWithGivenDirectSum", pre_function := function( cat, diagram, test_object, source, direct_sum ) @@ -742,20 +862,28 @@ UniversalMorphismIntoDirectSumWithGivenDirectSum := rec( InjectionOfCofactorOfDirectSum := rec( filter_list := [ "category", "list_of_objects", "integer" ], - io_type := [ [ "objects", "k" ], [ "objects_k", "P" ] ], + input_arguments_names := [ "cat", "objects", "k" ], + output_source_getter_string := "objects[k]", + output_source_getter_preconditions := [ ], with_given_object_position := "Range", return_type := "morphism", dual_operation := "ProjectionInFactorOfDirectSum" ), InjectionOfCofactorOfDirectSumWithGivenDirectSum := rec( filter_list := [ "category", "list_of_objects", "integer", "object" ], - io_type := [ [ "objects", "k", "P" ], [ "objects_k", "P" ] ], + input_arguments_names := [ "cat", "objects", "k", "P" ], + output_source_getter_string := "objects[k]", + output_source_getter_preconditions := [ ], + output_range_getter_string := "P", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "ProjectionInFactorOfDirectSumWithGivenDirectSum" ), UniversalMorphismFromDirectSum := rec( filter_list := [ "category", "list_of_objects", "object", "list_of_morphisms" ], - io_type := [ [ "objects", "T", "tau" ], [ "P", "T" ] ], + input_arguments_names := [ "cat", "objects", "T", "tau" ], + output_range_getter_string := "T", + output_range_getter_preconditions := [ ], with_given_object_position := "Source", dual_operation := "UniversalMorphismIntoDirectSum", @@ -781,7 +909,11 @@ UniversalMorphismFromDirectSum := rec( UniversalMorphismFromDirectSumWithGivenDirectSum := rec( filter_list := [ "category", "list_of_objects", "object", "list_of_morphisms", "object" ], - io_type := [ [ "objects", "T", "tau", "P" ], [ "P", "T" ] ], + input_arguments_names := [ "cat", "objects", "T", "tau", "P" ], + output_source_getter_string := "P", + output_source_getter_preconditions := [ ], + output_range_getter_string := "T", + output_range_getter_preconditions := [ ], dual_operation := "UniversalMorphismIntoDirectSumWithGivenDirectSum", pre_function := function( cat, diagram, test_object, sink, direct_sum ) @@ -814,14 +946,20 @@ TerminalObject := rec( UniversalMorphismIntoTerminalObject := rec( filter_list := [ "category", "object" ], - io_type := [ [ "T" ], [ "T", "P" ] ], + input_arguments_names := [ "cat", "T" ], + output_source_getter_string := "T", + output_source_getter_preconditions := [ ], with_given_object_position := "Range", return_type := "morphism", dual_operation := "UniversalMorphismFromInitialObject" ), UniversalMorphismIntoTerminalObjectWithGivenTerminalObject := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "T", "P" ], [ "T", "P" ] ], + input_arguments_names := [ "cat", "T", "P" ], + output_source_getter_string := "T", + output_source_getter_preconditions := [ ], + output_range_getter_string := "P", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "UniversalMorphismFromInitialObjectWithGivenInitialObject" ), @@ -835,14 +973,20 @@ InitialObject := rec( UniversalMorphismFromInitialObject := rec( filter_list := [ "category", "object" ], - io_type := [ [ "T" ], [ "P", "T" ] ], + input_arguments_names := [ "cat", "T" ], + output_range_getter_string := "T", + output_range_getter_preconditions := [ ], with_given_object_position := "Source", return_type := "morphism", dual_operation := "UniversalMorphismIntoTerminalObject" ), UniversalMorphismFromInitialObjectWithGivenInitialObject := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "T", "P" ], [ "P", "T" ] ], + input_arguments_names := [ "cat", "T", "P" ], + output_source_getter_string := "P", + output_source_getter_preconditions := [ ], + output_range_getter_string := "T", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "UniversalMorphismIntoTerminalObjectWithGivenTerminalObject" ), @@ -856,20 +1000,28 @@ DirectProduct := rec( ProjectionInFactorOfDirectProduct := rec( filter_list := [ "category", "list_of_objects", "integer" ], - io_type := [ [ "objects", "k" ], [ "P", "objects_k" ] ], + input_arguments_names := [ "cat", "objects", "k" ], + output_range_getter_string := "objects[k]", + output_range_getter_preconditions := [ ], with_given_object_position := "Source", return_type := "morphism", dual_operation := "InjectionOfCofactorOfCoproduct" ), ProjectionInFactorOfDirectProductWithGivenDirectProduct := rec( filter_list := [ "category", "list_of_objects", "integer", "object" ], - io_type := [ [ "objects", "k", "P" ], [ "P", "objects_k" ] ], + input_arguments_names := [ "cat", "objects", "k", "P" ], + output_source_getter_string := "P", + output_source_getter_preconditions := [ ], + output_range_getter_string := "objects[k]", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "InjectionOfCofactorOfCoproductWithGivenCoproduct" ), UniversalMorphismIntoDirectProduct := rec( filter_list := [ "category", "list_of_objects", "object", "list_of_morphisms" ], - io_type := [ [ "objects", "T", "tau" ], [ "T", "P" ] ], + input_arguments_names := [ "cat", "objects", "T", "tau" ], + output_source_getter_string := "T", + output_source_getter_preconditions := [ ], with_given_object_position := "Range", dual_operation := "UniversalMorphismFromCoproduct", @@ -895,7 +1047,11 @@ UniversalMorphismIntoDirectProduct := rec( UniversalMorphismIntoDirectProductWithGivenDirectProduct := rec( filter_list := [ "category", "list_of_objects", "object", "list_of_morphisms", "object" ], - io_type := [ [ "objects", "T", "tau", "P" ], [ "T", "P" ] ], + input_arguments_names := [ "cat", "objects", "T", "tau", "P" ], + output_source_getter_string := "T", + output_source_getter_preconditions := [ ], + output_range_getter_string := "P", + output_range_getter_preconditions := [ ], dual_operation := "UniversalMorphismFromCoproductWithGivenCoproduct", pre_function := function( cat, diagram, test_object, source, direct_product ) @@ -920,7 +1076,11 @@ UniversalMorphismIntoDirectProductWithGivenDirectProduct := rec( ComponentOfMorphismIntoDirectProduct := rec( filter_list := [ "category", "morphism", "list_of_objects", "integer" ], - io_type := [ [ "alpha", "P", "i" ], [ "alpha_source", "P_i" ] ], + input_arguments_names := [ "cat", "alpha", "P", "i" ], + output_source_getter_string := "Source( alpha )", + output_source_getter_preconditions := [ ], + output_range_getter_string := "P[i]", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "ComponentOfMorphismFromCoproduct" ), @@ -1091,7 +1251,11 @@ IsZeroForMorphisms := rec( AdditionForMorphisms := rec( filter_list := [ "category", "morphism", "morphism" ], - io_type := [ [ "alpha", "beta" ], [ "alpha_source", "alpha_range" ] ], + input_arguments_names := [ "cat", "alpha", "beta" ], + output_source_getter_string := "Source( alpha )", + output_source_getter_preconditions := [ ], + output_range_getter_string := "Range( alpha )", + output_range_getter_preconditions := [ ], dual_operation := "AdditionForMorphisms", pre_function := function( cat, morphism_1, morphism_2 ) @@ -1117,7 +1281,11 @@ AdditionForMorphisms := rec( SubtractionForMorphisms := rec( filter_list := [ "category", "morphism", "morphism" ], - io_type := [ [ "alpha", "beta" ], [ "alpha_source", "alpha_range" ] ], + input_arguments_names := [ "cat", "alpha", "beta" ], + output_source_getter_string := "Source( alpha )", + output_source_getter_preconditions := [ ], + output_range_getter_string := "Range( alpha )", + output_range_getter_preconditions := [ ], dual_operation := "SubtractionForMorphisms", pre_function := function( cat, morphism_1, morphism_2 ) @@ -1143,7 +1311,11 @@ SubtractionForMorphisms := rec( MultiplyWithElementOfCommutativeRingForMorphisms := rec( filter_list := [ "category", "element_of_commutative_ring_of_linear_structure", "morphism" ], - io_type := [ [ "r", "alpha" ], [ "alpha_source", "alpha_range" ] ], + input_arguments_names := [ "cat", "r", "alpha" ], + output_source_getter_string := "Source( alpha )", + output_source_getter_preconditions := [ ], + output_range_getter_string := "Range( alpha )", + output_range_getter_preconditions := [ ], pre_function := function( cat, r, morphism ) @@ -1162,7 +1334,11 @@ MultiplyWithElementOfCommutativeRingForMorphisms := rec( AdditiveInverseForMorphisms := rec( filter_list := [ "category", "morphism" ], - io_type := [ [ "alpha" ], [ "alpha_source", "alpha_range" ] ], + input_arguments_names := [ "cat", "alpha" ], + output_source_getter_string := "Source( alpha )", + output_source_getter_preconditions := [ ], + output_range_getter_string := "Range( alpha )", + output_range_getter_preconditions := [ ], dual_operation := "AdditiveInverseForMorphisms", return_type := "morphism", compatible_with_congruence_of_morphisms := true, @@ -1178,20 +1354,28 @@ Coproduct := rec( InjectionOfCofactorOfCoproduct := rec( filter_list := [ "category", "list_of_objects", "integer" ], - io_type := [ [ "objects", "k" ], [ "objects_k", "P" ] ], + input_arguments_names := [ "cat", "objects", "k" ], + output_source_getter_string := "objects[k]", + output_source_getter_preconditions := [ ], with_given_object_position := "Range", return_type := "morphism", dual_operation := "ProjectionInFactorOfDirectProduct" ), InjectionOfCofactorOfCoproductWithGivenCoproduct := rec( filter_list := [ "category", "list_of_objects", "integer", "object" ], - io_type := [ [ "objects", "k", "P" ], [ "objects_k", "P" ] ], + input_arguments_names := [ "cat", "objects", "k", "P" ], + output_source_getter_string := "objects[k]", + output_source_getter_preconditions := [ ], + output_range_getter_string := "P", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "ProjectionInFactorOfDirectProductWithGivenDirectProduct" ), UniversalMorphismFromCoproduct := rec( filter_list := [ "category", "list_of_objects", "object", "list_of_morphisms" ], - io_type := [ [ "objects", "T", "tau" ], [ "P", "T" ] ], + input_arguments_names := [ "cat", "objects", "T", "tau" ], + output_range_getter_string := "T", + output_range_getter_preconditions := [ ], with_given_object_position := "Source", dual_operation := "UniversalMorphismIntoDirectProduct", @@ -1217,7 +1401,11 @@ UniversalMorphismFromCoproduct := rec( UniversalMorphismFromCoproductWithGivenCoproduct := rec( filter_list := [ "category", "list_of_objects", "object", "list_of_morphisms", "object" ], - io_type := [ [ "objects", "T", "tau", "P" ], [ "P", "T" ] ], + input_arguments_names := [ "cat", "objects", "T", "tau", "P" ], + output_source_getter_string := "P", + output_source_getter_preconditions := [ ], + output_range_getter_string := "T", + output_range_getter_preconditions := [ ], dual_operation := "UniversalMorphismIntoDirectProductWithGivenDirectProduct", pre_function := function( cat, diagram, test_object, sink, coproduct ) @@ -1242,7 +1430,11 @@ UniversalMorphismFromCoproductWithGivenCoproduct := rec( ComponentOfMorphismFromCoproduct := rec( filter_list := [ "category", "morphism", "list_of_objects", "integer" ], - io_type := [ [ "alpha", "I", "i" ], [ "I_i", "alpha_range" ] ], + input_arguments_names := [ "cat", "alpha", "I", "i" ], + output_source_getter_string := "I[i]", + output_source_getter_preconditions := [ ], + output_range_getter_string := "Range( alpha )", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "ComponentOfMorphismIntoDirectProduct" ), @@ -1338,7 +1530,9 @@ Equalizer := rec( EmbeddingOfEqualizer := rec( filter_list := [ "category", "object", "list_of_morphisms" ], return_type := "morphism", - io_type := [ [ "Y", "morphisms" ], [ "P", "Y" ] ], + input_arguments_names := [ "cat", "Y", "morphisms" ], + output_range_getter_string := "Y", + output_range_getter_preconditions := [ ], with_given_object_position := "Source", dual_operation := "ProjectionOntoCoequalizer", @@ -1349,14 +1543,20 @@ EmbeddingOfEqualizer := rec( EmbeddingOfEqualizerWithGivenEqualizer := rec( filter_list := [ "category", "object", "list_of_morphisms", "object" ], return_type := "morphism", - io_type := [ [ "Y", "morphisms", "P" ], [ "P", "Y" ] ], + input_arguments_names := [ "cat", "Y", "morphisms", "P" ], + output_source_getter_string := "P", + output_source_getter_preconditions := [ ], + output_range_getter_string := "Y", + output_range_getter_preconditions := [ ], dual_operation := "ProjectionOntoCoequalizerWithGivenCoequalizer", compatible_with_congruence_of_morphisms := false, ), MorphismFromEqualizerToSink := rec( filter_list := [ "category", "object", "list_of_morphisms" ], - io_type := [ [ "Y", "morphisms" ], [ "P", "morphisms_1_range" ] ], + input_arguments_names := [ "cat", "Y", "morphisms" ], + output_range_getter_string := "Range( morphisms[1] )", + output_range_getter_preconditions := [ ], with_given_object_position := "Source", dual_operation := "MorphismFromSourceToCoequalizer", return_type := "morphism", @@ -1365,7 +1565,11 @@ MorphismFromEqualizerToSink := rec( MorphismFromEqualizerToSinkWithGivenEqualizer := rec( filter_list := [ "category", "object", "list_of_morphisms", "object" ], - io_type := [ [ "Y", "morphisms", "P" ], [ "P", "morphisms_1_range" ] ], + input_arguments_names := [ "cat", "Y", "morphisms", "P" ], + output_source_getter_string := "P", + output_source_getter_preconditions := [ ], + output_range_getter_string := "Range( morphisms[1] )", + output_range_getter_preconditions := [ ], dual_operation := "MorphismFromSourceToCoequalizerWithGivenCoequalizer", return_type := "morphism", compatible_with_congruence_of_morphisms := false, @@ -1373,7 +1577,9 @@ MorphismFromEqualizerToSinkWithGivenEqualizer := rec( UniversalMorphismIntoEqualizer := rec( filter_list := [ "category", "object", "list_of_morphisms", "object", "morphism" ], - io_type := [ [ "Y", "morphisms", "T", "tau" ], [ "T", "P" ] ], + input_arguments_names := [ "cat", "Y", "morphisms", "T", "tau" ], + output_source_getter_string := "T", + output_source_getter_preconditions := [ ], with_given_object_position := "Range", return_type := "morphism", dual_operation := "UniversalMorphismFromCoequalizer", @@ -1420,7 +1626,11 @@ UniversalMorphismIntoEqualizer := rec( UniversalMorphismIntoEqualizerWithGivenEqualizer := rec( filter_list := [ "category", "object", "list_of_morphisms", "object", "morphism", "object" ], - io_type := [ [ "Y", "morphisms", "T", "tau", "P" ], [ "T", "P" ] ], + input_arguments_names := [ "cat", "Y", "morphisms", "T", "tau", "P" ], + output_source_getter_string := "T", + output_source_getter_preconditions := [ ], + output_range_getter_string := "P", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "UniversalMorphismFromCoequalizerWithGivenCoequalizer", compatible_with_congruence_of_morphisms := false, @@ -1428,14 +1638,14 @@ UniversalMorphismIntoEqualizerWithGivenEqualizer := rec( IsomorphismFromEqualizerToKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProduct := rec( filter_list := [ "category", "object", "list_of_morphisms" ], - io_type := [ [ "A", "D" ], [ "E", "Delta" ] ], + input_arguments_names := [ "cat", "A", "D" ], return_type := "morphism", dual_operation := "IsomorphismFromCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproductToCoequalizer", ), IsomorphismFromKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProductToEqualizer := rec( filter_list := [ "category", "object", "list_of_morphisms" ], - io_type := [ [ "A", "D" ], [ "Delta", "E" ] ], + input_arguments_names := [ "cat", "A", "D" ], return_type := "morphism", dual_operation := "IsomorphismFromCoequalizerToCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproduct", ), @@ -1473,7 +1683,9 @@ FiberProduct := rec( ProjectionInFactorOfFiberProduct := rec( filter_list := [ "category", "list_of_morphisms", "integer" ], - io_type := [ [ "morphisms", "k" ], [ "P", "morphisms_k_source" ] ], + input_arguments_names := [ "cat", "morphisms", "k" ], + output_range_getter_string := "Source( morphisms[k] )", + output_range_getter_preconditions := [ ], with_given_object_position := "Source", dual_operation := "InjectionOfCofactorOfPushout", @@ -1502,7 +1714,11 @@ ProjectionInFactorOfFiberProduct := rec( ProjectionInFactorOfFiberProductWithGivenFiberProduct := rec( filter_list := [ "category", "list_of_morphisms", "integer", "object" ], - io_type := [ [ "morphisms", "k", "P" ], [ "P", "morphisms_k_source" ] ], + input_arguments_names := [ "cat", "morphisms", "k", "P" ], + output_source_getter_string := "P", + output_source_getter_preconditions := [ ], + output_range_getter_string := "Source( morphisms[k] )", + output_range_getter_preconditions := [ ], dual_operation := "InjectionOfCofactorOfPushoutWithGivenPushout", pre_function := function( cat, diagram, projection_number, pullback ) @@ -1530,7 +1746,9 @@ ProjectionInFactorOfFiberProductWithGivenFiberProduct := rec( MorphismFromFiberProductToSink := rec( filter_list := [ "category", "list_of_morphisms" ], - io_type := [ [ "morphisms" ], [ "P", "morphisms_1_range" ] ], + input_arguments_names := [ "cat", "morphisms" ], + output_range_getter_string := "Range( morphisms[1] )", + output_range_getter_preconditions := [ ], with_given_object_position := "Source", dual_operation := "MorphismFromSourceToPushout", @@ -1555,7 +1773,11 @@ MorphismFromFiberProductToSink := rec( MorphismFromFiberProductToSinkWithGivenFiberProduct := rec( filter_list := [ "category", "list_of_morphisms", "object" ], - io_type := [ [ "morphisms", "P" ], [ "P", "morphisms_1_range" ] ], + input_arguments_names := [ "cat", "morphisms", "P" ], + output_source_getter_string := "P", + output_source_getter_preconditions := [ ], + output_range_getter_string := "Range( morphisms[1] )", + output_range_getter_preconditions := [ ], dual_operation := "MorphismFromSourceToPushoutWithGivenPushout", pre_function := function( cat, diagram, pullback ) @@ -1579,7 +1801,9 @@ MorphismFromFiberProductToSinkWithGivenFiberProduct := rec( UniversalMorphismIntoFiberProduct := rec( filter_list := [ "category", "list_of_morphisms", "object", "list_of_morphisms" ], - io_type := [ [ "morphisms", "T", "tau" ], [ "T", "P" ] ], + input_arguments_names := [ "cat", "morphisms", "T", "tau" ], + output_source_getter_string := "T", + output_source_getter_preconditions := [ ], with_given_object_position := "Range", dual_operation := "UniversalMorphismFromPushout", @@ -1630,7 +1854,11 @@ UniversalMorphismIntoFiberProduct := rec( UniversalMorphismIntoFiberProductWithGivenFiberProduct := rec( filter_list := [ "category", "list_of_morphisms", "object", "list_of_morphisms", "object" ], - io_type := [ [ "morphisms", "T", "tau", "P" ], [ "T", "P" ] ], + input_arguments_names := [ "cat", "morphisms", "T", "tau", "P" ], + output_source_getter_string := "T", + output_source_getter_preconditions := [ ], + output_range_getter_string := "P", + output_range_getter_preconditions := [ ], dual_operation := "UniversalMorphismFromPushoutWithGivenPushout", pre_function := function( cat, diagram, test_object, source, pullback ) @@ -1720,7 +1948,9 @@ Coequalizer := rec( ProjectionOntoCoequalizer := rec( filter_list := [ "category", "object", "list_of_morphisms" ], return_type := "morphism", - io_type := [ [ "Y", "morphisms" ], [ "Y", "P" ] ], + input_arguments_names := [ "cat", "Y", "morphisms" ], + output_source_getter_string := "Y", + output_source_getter_preconditions := [ ], with_given_object_position := "Range", dual_operation := "EmbeddingOfEqualizer", @@ -1731,14 +1961,20 @@ ProjectionOntoCoequalizer := rec( ProjectionOntoCoequalizerWithGivenCoequalizer := rec( filter_list := [ "category", "object", "list_of_morphisms", "object" ], return_type := "morphism", - io_type := [ [ "Y", "morphisms", "P" ], [ "Y", "P" ] ], + input_arguments_names := [ "cat", "Y", "morphisms", "P" ], + output_source_getter_string := "Y", + output_source_getter_preconditions := [ ], + output_range_getter_string := "P", + output_range_getter_preconditions := [ ], dual_operation := "EmbeddingOfEqualizerWithGivenEqualizer", compatible_with_congruence_of_morphisms := false, ), MorphismFromSourceToCoequalizer := rec( filter_list := [ "category", "object", "list_of_morphisms" ], - io_type := [ [ "Y", "morphisms" ], [ "morphisms_1_source", "P" ] ], + input_arguments_names := [ "cat", "Y", "morphisms" ], + output_source_getter_string := "Source( morphisms[1] )", + output_source_getter_preconditions := [ ], with_given_object_position := "Range", dual_operation := "MorphismFromEqualizerToSink", return_type := "morphism", @@ -1747,7 +1983,11 @@ MorphismFromSourceToCoequalizer := rec( MorphismFromSourceToCoequalizerWithGivenCoequalizer := rec( filter_list := [ "category", "object", "list_of_morphisms", "object" ], - io_type := [ [ "Y", "morphisms", "P" ], [ "morphisms_1_source", "P" ] ], + input_arguments_names := [ "cat", "Y", "morphisms", "P" ], + output_source_getter_string := "Source( morphisms[1] )", + output_source_getter_preconditions := [ ], + output_range_getter_string := "P", + output_range_getter_preconditions := [ ], dual_operation := "MorphismFromEqualizerToSinkWithGivenEqualizer", return_type := "morphism", compatible_with_congruence_of_morphisms := false, @@ -1755,7 +1995,9 @@ MorphismFromSourceToCoequalizerWithGivenCoequalizer := rec( UniversalMorphismFromCoequalizer := rec( filter_list := [ "category", "object", "list_of_morphisms", "object", "morphism" ], - io_type := [ [ "Y", "morphisms", "T", "tau" ], [ "P", "T" ] ], + input_arguments_names := [ "cat", "Y", "morphisms", "T", "tau" ], + output_range_getter_string := "T", + output_range_getter_preconditions := [ ], with_given_object_position := "Source", return_type := "morphism", dual_operation := "UniversalMorphismIntoEqualizer", @@ -1802,7 +2044,11 @@ UniversalMorphismFromCoequalizer := rec( UniversalMorphismFromCoequalizerWithGivenCoequalizer := rec( filter_list := [ "category", "object", "list_of_morphisms", "object", "morphism", "object" ], - io_type := [ [ "Y", "morphisms", "T", "tau", "P" ], [ "P", "T" ] ], + input_arguments_names := [ "cat", "Y", "morphisms", "T", "tau", "P" ], + output_source_getter_string := "P", + output_source_getter_preconditions := [ ], + output_range_getter_string := "T", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "UniversalMorphismIntoEqualizerWithGivenEqualizer", compatible_with_congruence_of_morphisms := false, @@ -1810,14 +2056,14 @@ UniversalMorphismFromCoequalizerWithGivenCoequalizer := rec( IsomorphismFromCoequalizerToCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproduct := rec( filter_list := [ "category", "object", "list_of_morphisms" ], - io_type := [ [ "A", "D" ], [ "C", "Delta" ] ], + input_arguments_names := [ "cat", "A", "D" ], return_type := "morphism", dual_operation := "IsomorphismFromKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProductToEqualizer", ), IsomorphismFromCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproductToCoequalizer := rec( filter_list := [ "category", "object", "list_of_morphisms" ], - io_type := [ [ "A", "D" ], [ "Delta", "C" ] ], + input_arguments_names := [ "cat", "A", "D" ], return_type := "morphism", dual_operation := "IsomorphismFromEqualizerToKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProduct", ), @@ -1855,7 +2101,9 @@ Pushout := rec( InjectionOfCofactorOfPushout := rec( filter_list := [ "category", "list_of_morphisms", "integer" ], - io_type := [ [ "morphisms", "k" ], [ "morphisms_k_range", "P" ] ], + input_arguments_names := [ "cat", "morphisms", "k" ], + output_source_getter_string := "Range( morphisms[k] )", + output_source_getter_preconditions := [ ], with_given_object_position := "Range", dual_operation := "ProjectionInFactorOfFiberProduct", @@ -1884,7 +2132,11 @@ InjectionOfCofactorOfPushout := rec( InjectionOfCofactorOfPushoutWithGivenPushout := rec( filter_list := [ "category", "list_of_morphisms", "integer", "object" ], - io_type := [ [ "morphisms", "k", "P" ], [ "morphisms_k_range", "P" ] ], + input_arguments_names := [ "cat", "morphisms", "k", "P" ], + output_source_getter_string := "Range( morphisms[k] )", + output_source_getter_preconditions := [ ], + output_range_getter_string := "P", + output_range_getter_preconditions := [ ], dual_operation := "ProjectionInFactorOfFiberProductWithGivenFiberProduct", pre_function := function( cat, diagram, injection_number, pushout ) @@ -1912,7 +2164,9 @@ InjectionOfCofactorOfPushoutWithGivenPushout := rec( MorphismFromSourceToPushout := rec( filter_list := [ "category", "list_of_morphisms" ], - io_type := [ [ "morphisms" ], [ "morphisms_1_source", "P" ] ], + input_arguments_names := [ "cat", "morphisms" ], + output_source_getter_string := "Source( morphisms[1] )", + output_source_getter_preconditions := [ ], with_given_object_position := "Range", dual_operation := "MorphismFromFiberProductToSink", @@ -1937,7 +2191,11 @@ MorphismFromSourceToPushout := rec( MorphismFromSourceToPushoutWithGivenPushout := rec( filter_list := [ "category", "list_of_morphisms", "object" ], - io_type := [ [ "morphisms", "P" ], [ "morphisms_1_source", "P" ] ], + input_arguments_names := [ "cat", "morphisms", "P" ], + output_source_getter_string := "Source( morphisms[1] )", + output_source_getter_preconditions := [ ], + output_range_getter_string := "P", + output_range_getter_preconditions := [ ], dual_operation := "MorphismFromFiberProductToSinkWithGivenFiberProduct", pre_function := function( cat, diagram, pushout ) @@ -1961,7 +2219,9 @@ MorphismFromSourceToPushoutWithGivenPushout := rec( UniversalMorphismFromPushout := rec( filter_list := [ "category", "list_of_morphisms", "object", "list_of_morphisms" ], - io_type := [ [ "morphisms", "T", "tau" ], [ "P", "T" ] ], + input_arguments_names := [ "cat", "morphisms", "T", "tau" ], + output_range_getter_string := "T", + output_range_getter_preconditions := [ ], with_given_object_position := "Source", dual_operation := "UniversalMorphismIntoFiberProduct", @@ -2012,7 +2272,11 @@ UniversalMorphismFromPushout := rec( UniversalMorphismFromPushoutWithGivenPushout := rec( filter_list := [ "category", "list_of_morphisms", "object", "list_of_morphisms", "object" ], - io_type := [ [ "morphisms", "T", "tau", "P" ], [ "P", "T" ] ], + input_arguments_names := [ "cat", "morphisms", "T", "tau", "P" ], + output_source_getter_string := "P", + output_source_getter_preconditions := [ ], + output_range_getter_string := "T", + output_range_getter_preconditions := [ ], dual_operation := "UniversalMorphismIntoFiberProductWithGivenFiberProduct", pre_function := function( cat, diagram, test_object, sink, pushout ) @@ -2069,14 +2333,20 @@ ImageObject := rec( ImageEmbedding := rec( filter_list := [ "category", "morphism" ], - io_type := [ [ "alpha" ], [ "I", "alpha_range" ] ], + input_arguments_names := [ "cat", "alpha" ], + output_range_getter_string := "Range( alpha )", + output_range_getter_preconditions := [ ], with_given_object_position := "Source", return_type := "morphism", dual_operation := "CoimageProjection" ), ImageEmbeddingWithGivenImageObject := rec( filter_list := [ "category", "morphism", "object" ], - io_type := [ [ "alpha", "I" ], [ "I", "alpha_range" ] ], + input_arguments_names := [ "cat", "alpha", "I" ], + output_source_getter_string := "I", + output_source_getter_preconditions := [ ], + output_range_getter_string := "Range( alpha )", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "CoimageProjectionWithGivenCoimageObject" ), @@ -2089,33 +2359,47 @@ CoimageObject := rec( CoimageProjection := rec( filter_list := [ "category", "morphism" ], - io_type := [ [ "alpha" ], [ "alpha_source", "C" ] ], + input_arguments_names := [ "cat", "alpha" ], + output_source_getter_string := "Source( alpha )", + output_source_getter_preconditions := [ ], with_given_object_position := "Range", return_type := "morphism", dual_operation := "ImageEmbedding" ), CoimageProjectionWithGivenCoimageObject := rec( filter_list := [ "category", "morphism", "object" ], - io_type := [ [ "alpha", "C" ], [ "alpha_source", "C" ] ], + input_arguments_names := [ "cat", "alpha", "C" ], + output_source_getter_string := "Source( alpha )", + output_source_getter_preconditions := [ ], + output_range_getter_string := "C", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "ImageEmbeddingWithGivenImageObject" ), AstrictionToCoimage := rec( filter_list := [ "category", "morphism" ], - io_type := [ [ "alpha" ], [ "C", "alpha_range" ] ], + input_arguments_names := [ "cat", "alpha" ], + output_range_getter_string := "Range( alpha )", + output_range_getter_preconditions := [ ], with_given_object_position := "Source", return_type := "morphism", dual_operation := "CoastrictionToImage" ), AstrictionToCoimageWithGivenCoimageObject := rec( filter_list := [ "category", "morphism", "object" ], - io_type := [ [ "alpha", "C" ], [ "C", "alpha_range" ] ], + input_arguments_names := [ "cat", "alpha", "C" ], + output_source_getter_string := "C", + output_source_getter_preconditions := [ ], + output_range_getter_string := "Range( alpha )", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "CoastrictionToImageWithGivenImageObject" ), UniversalMorphismIntoCoimage := rec( filter_list := [ "category", "morphism", "pair_of_morphisms" ], - io_type := [ [ "alpha", "tau" ], [ "tau_1_range", "C" ] ], + input_arguments_names := [ "cat", "alpha", "tau" ], + output_source_getter_string := "Range( tau[1] )", + output_source_getter_preconditions := [ ], with_given_object_position := "Range", dual_preprocessor_func := CAP_INTERNAL_REVERSE_LISTS_IN_ARGUMENTS_FOR_OPPOSITE, pre_function := function( cat, morphism, test_factorization ) @@ -2139,7 +2423,11 @@ UniversalMorphismIntoCoimage := rec( UniversalMorphismIntoCoimageWithGivenCoimageObject := rec( filter_list := [ "category", "morphism", "pair_of_morphisms", "object" ], - io_type := [ [ "alpha", "tau", "C" ], [ "tau_1_range", "C" ] ], + input_arguments_names := [ "cat", "alpha", "tau", "C" ], + output_source_getter_string := "Range( tau[1] )", + output_source_getter_preconditions := [ ], + output_range_getter_string := "C", + output_range_getter_preconditions := [ ], dual_preprocessor_func := CAP_INTERNAL_REVERSE_LISTS_IN_ARGUMENTS_FOR_OPPOSITE, pre_function := function( cat, morphism, test_factorization, image ) @@ -2162,14 +2450,22 @@ UniversalMorphismIntoCoimageWithGivenCoimageObject := rec( MorphismFromCoimageToImageWithGivenObjects := rec( filter_list := [ "category", "object", "morphism", "object" ], - io_type := [ [ "C", "alpha", "I" ], [ "C", "I" ] ], + input_arguments_names := [ "cat", "C", "alpha", "I" ], + output_source_getter_string := "C", + output_source_getter_preconditions := [ ], + output_range_getter_string := "I", + output_range_getter_preconditions := [ ], dual_operation := "MorphismFromCoimageToImageWithGivenObjects", dual_arguments_reversed := true, return_type := "morphism" ), InverseMorphismFromCoimageToImageWithGivenObjects := rec( filter_list := [ "category", "object", "morphism", "object" ], - io_type := [ [ "C", "alpha", "I" ], [ "I", "C" ] ], + input_arguments_names := [ "cat", "C", "alpha", "I" ], + output_source_getter_string := "I", + output_source_getter_preconditions := [ ], + output_range_getter_string := "C", + output_range_getter_preconditions := [ ], dual_operation := "InverseMorphismFromCoimageToImageWithGivenObjects", dual_arguments_reversed := true, return_type := "morphism" ), @@ -2333,20 +2629,28 @@ IsEqualToZeroMorphism := rec( CoastrictionToImage := rec( filter_list := [ "category", "morphism" ], - io_type := [ [ "alpha" ], [ "alpha_source", "I" ] ], + input_arguments_names := [ "cat", "alpha" ], + output_source_getter_string := "Source( alpha )", + output_source_getter_preconditions := [ ], with_given_object_position := "Range", return_type := "morphism", dual_operation := "AstrictionToCoimage" ), CoastrictionToImageWithGivenImageObject := rec( filter_list := [ "category", "morphism", "object" ], - io_type := [ [ "alpha", "I" ], [ "alpha_source", "I" ] ], + input_arguments_names := [ "cat", "alpha", "I" ], + output_source_getter_string := "Source( alpha )", + output_source_getter_preconditions := [ ], + output_range_getter_string := "I", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "AstrictionToCoimageWithGivenCoimageObject" ), UniversalMorphismFromImage := rec( filter_list := [ "category", "morphism", "pair_of_morphisms" ], - io_type := [ [ "alpha", "tau" ], [ "I", "tau_1_range" ] ], + input_arguments_names := [ "cat", "alpha", "tau" ], + output_range_getter_string := "Range( tau[1] )", + output_range_getter_preconditions := [ ], with_given_object_position := "Source", dual_operation := "UniversalMorphismIntoCoimage", dual_preprocessor_func := CAP_INTERNAL_REVERSE_LISTS_IN_ARGUMENTS_FOR_OPPOSITE, @@ -2370,7 +2674,11 @@ UniversalMorphismFromImage := rec( UniversalMorphismFromImageWithGivenImageObject := rec( filter_list := [ "category", "morphism", "pair_of_morphisms", "object" ], - io_type := [ [ "alpha", "tau", "I" ], [ "I", "tau_1_range" ] ], + input_arguments_names := [ "cat", "alpha", "tau", "I" ], + output_source_getter_string := "I", + output_source_getter_preconditions := [ ], + output_range_getter_string := "Range( tau[1] )", + output_range_getter_preconditions := [ ], dual_operation := "UniversalMorphismIntoCoimageWithGivenCoimageObject", dual_preprocessor_func := CAP_INTERNAL_REVERSE_LISTS_IN_ARGUMENTS_FOR_OPPOSITE, pre_function := function( cat, morphism, test_factorization, image ) @@ -2407,7 +2715,11 @@ KernelObjectFunctorial := rec( KernelObjectFunctorialWithGivenKernelObjects := rec( filter_list := [ "category", "object", "morphism", "morphism", "morphism", "object" ], - io_type := [ [ "P", "alpha", "mu", "alphap", "Pp" ], [ "P", "Pp" ] ], + input_arguments_names := [ "cat", "P", "alpha", "mu", "alphap", "Pp" ], + output_source_getter_string := "P", + output_source_getter_preconditions := [ ], + output_range_getter_string := "Pp", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "CokernelObjectFunctorialWithGivenCokernelObjects", dual_arguments_reversed := true, @@ -2430,7 +2742,11 @@ CokernelObjectFunctorial := rec( CokernelObjectFunctorialWithGivenCokernelObjects := rec( filter_list := [ "category", "object", "morphism", "morphism", "morphism", "object" ], - io_type := [ [ "P", "alpha", "mu", "alphap", "Pp" ], [ "P", "Pp" ] ], + input_arguments_names := [ "cat", "P", "alpha", "mu", "alphap", "Pp" ], + output_source_getter_string := "P", + output_source_getter_preconditions := [ ], + output_range_getter_string := "Pp", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "KernelObjectFunctorialWithGivenKernelObjects", dual_arguments_reversed := true, @@ -2452,7 +2768,11 @@ TerminalObjectFunctorial := rec( TerminalObjectFunctorialWithGivenTerminalObjects := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "P", "Pp" ], [ "P", "Pp" ] ], + input_arguments_names := [ "cat", "P", "Pp" ], + output_source_getter_string := "P", + output_source_getter_preconditions := [ ], + output_range_getter_string := "Pp", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "InitialObjectFunctorialWithGivenInitialObjects", dual_arguments_reversed := true, @@ -2473,7 +2793,11 @@ InitialObjectFunctorial := rec( InitialObjectFunctorialWithGivenInitialObjects := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "P", "Pp" ], [ "P", "Pp" ] ], + input_arguments_names := [ "cat", "P", "Pp" ], + output_source_getter_string := "P", + output_source_getter_preconditions := [ ], + output_range_getter_string := "Pp", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "TerminalObjectFunctorialWithGivenTerminalObjects", dual_arguments_reversed := true, @@ -2495,7 +2819,11 @@ DirectProductFunctorial := rec( DirectProductFunctorialWithGivenDirectProducts := rec( filter_list := [ "category", "object", "list_of_objects", "list_of_morphisms", "list_of_objects", "object" ], - io_type := [ [ "P", "objects", "L", "objectsp", "Pp" ], [ "P", "Pp" ] ], + input_arguments_names := [ "cat", "P", "objects", "L", "objectsp", "Pp" ], + output_source_getter_string := "P", + output_source_getter_preconditions := [ ], + output_range_getter_string := "Pp", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "CoproductFunctorialWithGivenCoproducts", dual_arguments_reversed := true, @@ -2518,7 +2846,11 @@ CoproductFunctorial := rec( CoproductFunctorialWithGivenCoproducts := rec( filter_list := [ "category", "object", "list_of_objects", "list_of_morphisms", "list_of_objects", "object" ], - io_type := [ [ "P", "objects", "L", "objectsp", "Pp" ], [ "P", "Pp" ] ], + input_arguments_names := [ "cat", "P", "objects", "L", "objectsp", "Pp" ], + output_source_getter_string := "P", + output_source_getter_preconditions := [ ], + output_range_getter_string := "Pp", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "DirectProductFunctorialWithGivenDirectProducts", dual_arguments_reversed := true, @@ -2541,7 +2873,11 @@ DirectSumFunctorial := rec( DirectSumFunctorialWithGivenDirectSums := rec( filter_list := [ "category", "object", "list_of_objects", "list_of_morphisms", "list_of_objects", "object" ], - io_type := [ [ "P", "objects", "L", "objectsp", "Pp" ], [ "P", "Pp" ] ], + input_arguments_names := [ "cat", "P", "objects", "L", "objectsp", "Pp" ], + output_source_getter_string := "P", + output_source_getter_preconditions := [ ], + output_range_getter_string := "Pp", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "DirectSumFunctorialWithGivenDirectSums", dual_arguments_reversed := true, @@ -2564,7 +2900,11 @@ EqualizerFunctorial := rec( EqualizerFunctorialWithGivenEqualizers := rec( filter_list := [ "category", "object", "list_of_morphisms", "morphism", "list_of_morphisms", "object" ], - io_type := [ [ "P", "morphisms", "mu", "morphismsp", "Pp" ], [ "P", "Pp" ] ], + input_arguments_names := [ "cat", "P", "morphisms", "mu", "morphismsp", "Pp" ], + output_source_getter_string := "P", + output_source_getter_preconditions := [ ], + output_range_getter_string := "Pp", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "CoequalizerFunctorialWithGivenCoequalizers", dual_arguments_reversed := true, @@ -2587,7 +2927,11 @@ CoequalizerFunctorial := rec( CoequalizerFunctorialWithGivenCoequalizers := rec( filter_list := [ "category", "object", "list_of_morphisms", "morphism", "list_of_morphisms", "object" ], - io_type := [ [ "P", "morphisms", "mu", "morphismsp", "Pp" ], [ "P", "Pp" ] ], + input_arguments_names := [ "cat", "P", "morphisms", "mu", "morphismsp", "Pp" ], + output_source_getter_string := "P", + output_source_getter_preconditions := [ ], + output_range_getter_string := "Pp", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "EqualizerFunctorialWithGivenEqualizers", dual_arguments_reversed := true, @@ -2610,7 +2954,11 @@ FiberProductFunctorial := rec( FiberProductFunctorialWithGivenFiberProducts := rec( filter_list := [ "category", "object", "list_of_morphisms", "list_of_morphisms", "list_of_morphisms", "object" ], - io_type := [ [ "P", "morphisms", "L", "morphismsp", "Pp" ], [ "P", "Pp" ] ], + input_arguments_names := [ "cat", "P", "morphisms", "L", "morphismsp", "Pp" ], + output_source_getter_string := "P", + output_source_getter_preconditions := [ ], + output_range_getter_string := "Pp", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "PushoutFunctorialWithGivenPushouts", dual_arguments_reversed := true, @@ -2633,7 +2981,11 @@ PushoutFunctorial := rec( PushoutFunctorialWithGivenPushouts := rec( filter_list := [ "category", "object", "list_of_morphisms", "list_of_morphisms", "list_of_morphisms", "object" ], - io_type := [ [ "P", "morphisms", "L", "morphismsp", "Pp" ], [ "P", "Pp" ] ], + input_arguments_names := [ "cat", "P", "morphisms", "L", "morphismsp", "Pp" ], + output_source_getter_string := "P", + output_source_getter_preconditions := [ ], + output_range_getter_string := "Pp", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "FiberProductFunctorialWithGivenFiberProducts", dual_arguments_reversed := true, @@ -2655,7 +3007,11 @@ ImageObjectFunctorial := rec( ImageObjectFunctorialWithGivenImageObjects := rec( filter_list := [ "category", "object", "morphism", "morphism", "morphism", "object" ], - io_type := [ [ "I", "alpha", "nu", "alphap", "Ip" ], [ "I", "Ip" ] ], + input_arguments_names := [ "cat", "I", "alpha", "nu", "alphap", "Ip" ], + output_source_getter_string := "I", + output_source_getter_preconditions := [ ], + output_range_getter_string := "Ip", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "CoimageObjectFunctorialWithGivenCoimageObjects", dual_arguments_reversed := true, @@ -2676,7 +3032,11 @@ CoimageObjectFunctorial := rec( CoimageObjectFunctorialWithGivenCoimageObjects := rec( filter_list := [ "category", "object", "morphism", "morphism", "morphism", "object" ], - io_type := [ [ "C", "alpha", "mu", "alphap", "Cp" ], [ "C", "Cp" ] ], + input_arguments_names := [ "cat", "C", "alpha", "mu", "alphap", "Cp" ], + output_source_getter_string := "C", + output_source_getter_preconditions := [ ], + output_range_getter_string := "Cp", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "ImageObjectFunctorialWithGivenImageObjects", dual_arguments_reversed := true, @@ -2763,112 +3123,116 @@ IsWellDefinedForTwoCells := rec( JointPairwiseDifferencesOfMorphismsIntoDirectProduct := rec( filter_list := [ "category", "object", "list_of_morphisms" ], - io_type := [ [ "A", "D" ], [ "A", "P" ] ], + input_arguments_names := [ "cat", "A", "D" ], + output_source_getter_string := "A", + output_source_getter_preconditions := [ ], return_type := "morphism", dual_operation := "JointPairwiseDifferencesOfMorphismsFromCoproduct", ), IsomorphismFromFiberProductToEqualizerOfDirectProductDiagram := rec( filter_list := [ "category", "list_of_morphisms" ], - io_type := [ [ "D" ], [ "P", "Delta" ] ], + input_arguments_names := [ "cat", "D" ], return_type := "morphism", dual_operation := "IsomorphismFromCoequalizerOfCoproductDiagramToPushout", ), IsomorphismFromEqualizerOfDirectProductDiagramToFiberProduct := rec( filter_list := [ "category", "list_of_morphisms" ], - io_type := [ [ "D" ], [ "Delta", "P" ] ], + input_arguments_names := [ "cat", "D" ], return_type := "morphism", dual_operation := "IsomorphismFromPushoutToCoequalizerOfCoproductDiagram", ), IsomorphismFromPushoutToCoequalizerOfCoproductDiagram := rec( filter_list := [ "category", "list_of_morphisms" ], - io_type := [ [ "D" ], [ "P", "Delta" ] ], + input_arguments_names := [ "cat", "D" ], return_type := "morphism", dual_operation := "IsomorphismFromEqualizerOfDirectProductDiagramToFiberProduct", ), IsomorphismFromCoequalizerOfCoproductDiagramToPushout := rec( filter_list := [ "category", "list_of_morphisms" ], - io_type := [ [ "D" ], [ "Delta", "P" ] ], + input_arguments_names := [ "cat", "D" ], return_type := "morphism", dual_operation := "IsomorphismFromFiberProductToEqualizerOfDirectProductDiagram", ), IsomorphismFromImageObjectToKernelOfCokernel := rec( filter_list := [ "category", "morphism" ], - io_type := [ [ "alpha" ], [ "I", "P" ] ], + input_arguments_names := [ "cat", "alpha" ], return_type := "morphism", dual_operation := "IsomorphismFromCokernelOfKernelToCoimage", ), IsomorphismFromKernelOfCokernelToImageObject := rec( filter_list := [ "category", "morphism" ], - io_type := [ [ "alpha" ], [ "P", "I" ] ], + input_arguments_names := [ "cat", "alpha" ], return_type := "morphism", dual_operation := "IsomorphismFromCoimageToCokernelOfKernel", ), IsomorphismFromCoimageToCokernelOfKernel := rec( filter_list := [ "category", "morphism" ], - io_type := [ [ "alpha" ], [ "CI", "C" ] ], + input_arguments_names := [ "cat", "alpha" ], return_type := "morphism", dual_operation := "IsomorphismFromKernelOfCokernelToImageObject", ), IsomorphismFromCokernelOfKernelToCoimage := rec( filter_list := [ "category", "morphism" ], - io_type := [ [ "alpha" ], [ "I", "CI" ] ], + input_arguments_names := [ "cat", "alpha" ], return_type := "morphism", dual_operation := "IsomorphismFromImageObjectToKernelOfCokernel", ), CanonicalIdentificationFromImageObjectToCoimage := rec( filter_list := [ "category", "morphism" ], - io_type := [ [ "alpha" ], [ "I", "C" ] ], + input_arguments_names := [ "cat", "alpha" ], return_type := "morphism", dual_operation := "CanonicalIdentificationFromCoimageToImageObject", ), CanonicalIdentificationFromCoimageToImageObject := rec( filter_list := [ "category", "morphism" ], - io_type := [ [ "alpha" ], [ "C", "I" ] ], + input_arguments_names := [ "cat", "alpha" ], return_type := "morphism", dual_operation := "CanonicalIdentificationFromImageObjectToCoimage", ), IsomorphismFromDirectSumToDirectProduct := rec( filter_list := [ "category", "list_of_objects" ], - io_type := [ [ "D" ], [ "S", "P" ] ], + input_arguments_names := [ "cat", "D" ], return_type := "morphism", dual_operation := "IsomorphismFromCoproductToDirectSum", ), IsomorphismFromDirectSumToCoproduct := rec( filter_list := [ "category", "list_of_objects" ], - io_type := [ [ "D" ], [ "S", "C" ] ], + input_arguments_names := [ "cat", "D" ], return_type := "morphism", dual_operation := "IsomorphismFromDirectProductToDirectSum", ), IsomorphismFromDirectProductToDirectSum := rec( filter_list := [ "category", "list_of_objects" ], - io_type := [ [ "D" ], [ "P", "S" ] ], + input_arguments_names := [ "cat", "D" ], return_type := "morphism", dual_operation := "IsomorphismFromDirectSumToCoproduct", ), IsomorphismFromCoproductToDirectSum := rec( filter_list := [ "category", "list_of_objects" ], - io_type := [ [ "D" ], [ "C", "S" ] ], + input_arguments_names := [ "cat", "D" ], return_type := "morphism", dual_operation := "IsomorphismFromDirectSumToDirectProduct", ), JointPairwiseDifferencesOfMorphismsFromCoproduct := rec( filter_list := [ "category", "object", "list_of_morphisms" ], - io_type := [ [ "A", "D" ], [ "C", "A" ] ], + input_arguments_names := [ "cat", "A", "D" ], + output_range_getter_string := "A", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "JointPairwiseDifferencesOfMorphismsIntoDirectProduct", ), @@ -2881,7 +3245,9 @@ SomeProjectiveObject := rec( EpimorphismFromSomeProjectiveObject := rec( filter_list := [ "category", "object" ], - io_type := [ [ "A" ], [ "P", "A" ] ], + input_arguments_names := [ "cat", "A" ], + output_range_getter_string := "A", + output_range_getter_preconditions := [ ], with_given_object_position := "Source", return_type := "morphism", dual_operation := "MonomorphismIntoSomeInjectiveObject", @@ -2889,7 +3255,11 @@ EpimorphismFromSomeProjectiveObject := rec( EpimorphismFromSomeProjectiveObjectWithGivenSomeProjectiveObject := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "A", "P" ], [ "P", "A" ] ], + input_arguments_names := [ "cat", "A", "P" ], + output_source_getter_string := "P", + output_source_getter_preconditions := [ ], + output_range_getter_string := "A", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "MonomorphismIntoSomeInjectiveObjectWithGivenSomeInjectiveObject", is_merely_set_theoretic := true ), @@ -2902,7 +3272,9 @@ SomeInjectiveObject := rec( MonomorphismIntoSomeInjectiveObject := rec( filter_list := [ "category", "object" ], - io_type := [ [ "A" ], [ "A", "I" ] ], + input_arguments_names := [ "cat", "A" ], + output_source_getter_string := "A", + output_source_getter_preconditions := [ ], with_given_object_position := "Range", return_type := "morphism", dual_operation := "EpimorphismFromSomeProjectiveObject", @@ -2910,20 +3282,32 @@ MonomorphismIntoSomeInjectiveObject := rec( MonomorphismIntoSomeInjectiveObjectWithGivenSomeInjectiveObject := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "A", "I" ], [ "A", "I" ] ], + input_arguments_names := [ "cat", "A", "I" ], + output_source_getter_string := "A", + output_source_getter_preconditions := [ ], + output_range_getter_string := "I", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "EpimorphismFromSomeProjectiveObjectWithGivenSomeProjectiveObject", is_merely_set_theoretic := true ), ComponentOfMorphismIntoDirectSum := rec( filter_list := [ "category", "morphism", "list_of_objects", "integer" ], - io_type := [ [ "alpha", "S", "i" ], [ "alpha_source", "S_i" ] ], + input_arguments_names := [ "cat", "alpha", "S", "i" ], + output_source_getter_string := "Source( alpha )", + output_source_getter_preconditions := [ ], + output_range_getter_string := "S[i]", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "ComponentOfMorphismFromDirectSum" ), ComponentOfMorphismFromDirectSum := rec( filter_list := [ "category", "morphism", "list_of_objects", "integer" ], - io_type := [ [ "alpha", "S", "i" ], [ "S_i", "alpha_range" ] ], + input_arguments_names := [ "cat", "alpha", "S", "i" ], + output_source_getter_string := "S[i]", + output_source_getter_preconditions := [ ], + output_range_getter_string := "Range( alpha )", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "ComponentOfMorphismIntoDirectSum" ), @@ -2984,7 +3368,11 @@ MorphismBetweenDirectSums := rec( MorphismBetweenDirectSumsWithGivenDirectSums := rec( filter_list := [ "category", "object", "list_of_objects", "list_of_lists_of_morphisms", "list_of_objects", "object" ], - io_type := [ [ "S", "source_diagram", "mat", "range_diagram", "T" ], [ "S", "T" ] ], + input_arguments_names := [ "cat", "S", "source_diagram", "mat", "range_diagram", "T" ], + output_source_getter_string := "S", + output_source_getter_preconditions := [ ], + output_range_getter_string := "T", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "MorphismBetweenDirectSumsWithGivenDirectSums", dual_preprocessor_func := function( arg ) @@ -3171,28 +3559,36 @@ RandomObjectByInteger := rec( RandomMorphismByInteger := rec( filter_list := [ "category", "integer" ], - io_type := [ [ "n" ], [ "A", "B" ] ], + input_arguments_names := [ "cat", "n" ], return_type := "morphism", dual_operation := "RandomMorphismByInteger", ), RandomMorphismWithFixedSourceByInteger := rec( filter_list := [ "category", "object", "integer" ], - io_type := [ [ "A", "n" ], [ "A", "B" ] ], + input_arguments_names := [ "cat", "A", "n" ], + output_source_getter_string := "A", + output_source_getter_preconditions := [ ], return_type := "morphism", dual_operation := "RandomMorphismWithFixedRangeByInteger", ), RandomMorphismWithFixedRangeByInteger := rec( filter_list := [ "category", "object", "integer" ], - io_type := [ [ "B", "n" ], [ "A", "B" ] ], + input_arguments_names := [ "cat", "B", "n" ], + output_range_getter_string := "B", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "RandomMorphismWithFixedSourceByInteger", ), RandomMorphismWithFixedSourceAndRangeByInteger := rec( filter_list := [ "category", "object", "object", "integer" ], - io_type := [ [ "A", "B", "n" ], [ "A", "B" ] ], + input_arguments_names := [ "cat", "A", "B", "n" ], + output_source_getter_string := "A", + output_source_getter_preconditions := [ ], + output_range_getter_string := "B", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "RandomMorphismWithFixedSourceAndRangeByInteger", dual_preprocessor_func := function( cat, A, B, n ) @@ -3208,25 +3604,33 @@ RandomObjectByList := rec( RandomMorphismByList := rec( filter_list := [ "category", "arbitrary_list" ], - io_type := [ [ "L" ], [ "A", "B" ] ], + input_arguments_names := [ "cat", "L" ], return_type := "morphism" ), RandomMorphismWithFixedSourceByList := rec( filter_list := [ "category", "object", "arbitrary_list" ], - io_type := [ [ "A", "L" ], [ "A", "B" ] ], + input_arguments_names := [ "cat", "A", "L" ], + output_source_getter_string := "A", + output_source_getter_preconditions := [ ], return_type := "morphism", ), RandomMorphismWithFixedRangeByList := rec( filter_list := [ "category", "object", "arbitrary_list" ], - io_type := [ [ "B", "L" ], [ "A", "B" ] ], + input_arguments_names := [ "cat", "B", "L" ], + output_range_getter_string := "B", + output_range_getter_preconditions := [ ], return_type := "morphism" ), RandomMorphismWithFixedSourceAndRangeByList := rec( filter_list := [ "category", "object", "object", "arbitrary_list" ], - io_type := [ [ "A", "B", "L" ], [ "A", "B" ] ], + input_arguments_names := [ "cat", "A", "B", "L" ], + output_source_getter_string := "A", + output_source_getter_preconditions := [ ], + output_range_getter_string := "B", + output_range_getter_preconditions := [ ], return_type := "morphism" ), @@ -3250,7 +3654,7 @@ HomologyObject := rec( HomologyObjectFunctorialWithGivenHomologyObjects := rec( filter_list := [ "category", "object", "5_tuple_of_morphisms", "object" ], - io_type := [ [ "H_1", "L", "H_2" ], [ "H_1", "H_2" ] ], + input_arguments_names := [ "cat", "H_1", "L", "H_2" ], return_type := "morphism", pre_function := function( cat, H_1, L, H2 ) local alpha, beta, epsilon, gamma, delta; @@ -3302,12 +3706,12 @@ HomologyObjectFunctorialWithGivenHomologyObjects := rec( IsomorphismFromHomologyObjectToItsConstructionAsAnImageObject := rec( filter_list := [ "category", "morphism", "morphism" ], - io_type := [ [ "alpha", "beta" ], [ "A", "B" ] ], + input_arguments_names := [ "cat", "alpha", "beta" ], return_type := "morphism" ), IsomorphismFromItsConstructionAsAnImageObjectToHomologyObject := rec( filter_list := [ "category", "morphism", "morphism" ], - io_type := [ [ "alpha", "beta" ], [ "A", "B" ] ], + input_arguments_names := [ "cat", "alpha", "beta" ], return_type := "morphism" ), ## SimplifyObject* @@ -3338,7 +3742,9 @@ SimplifyObject := rec( SimplifyObject_IsoFromInputObject := rec( filter_list := [ "category", "object", "nonneg_integer_or_infinity" ], - io_type := [ [ "A", "n" ], [ "A", "B" ] ], + input_arguments_names := [ "cat", "A", "n" ], + output_source_getter_string := "A", + output_source_getter_preconditions := [ ], return_type := "morphism", dual_operation := "SimplifyObject_IsoToInputObject", redirect_function := function( cat, A, n ) @@ -3355,7 +3761,9 @@ SimplifyObject_IsoFromInputObject := rec( SimplifyObject_IsoToInputObject := rec( filter_list := [ "category", "object", "nonneg_integer_or_infinity" ], - io_type := [ [ "A", "n" ], [ "B", "A" ] ], + input_arguments_names := [ "cat", "A", "n" ], + output_range_getter_string := "A", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "SimplifyObject_IsoFromInputObject", redirect_function := "SimplifyObject_IsoFromInputObject", @@ -3365,7 +3773,11 @@ SimplifyObject_IsoToInputObject := rec( ## SimplifyMorphism SimplifyMorphism := rec( filter_list := [ "category", "morphism", "nonneg_integer_or_infinity" ], - io_type := [ [ "mor", "n" ], [ "mor_source", "mor_range" ] ], + input_arguments_names := [ "cat", "mor", "n" ], + output_source_getter_string := "Source( mor )", + output_source_getter_preconditions := [ ], + output_range_getter_string := "Range( mor )", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "SimplifyMorphism", redirect_function := "SimplifyObject", @@ -3375,7 +3787,9 @@ SimplifyMorphism := rec( ## SimplifySource* SimplifySource := rec( filter_list := [ "category", "morphism", "nonneg_integer_or_infinity" ], - io_type := [ [ "mor", "n" ], [ "Ap", "mor_range" ] ], + input_arguments_names := [ "cat", "mor", "n" ], + output_range_getter_string := "Range( mor )", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "SimplifyRange", redirect_function := "SimplifyObject", @@ -3384,7 +3798,9 @@ SimplifySource := rec( SimplifySource_IsoToInputObject := rec( filter_list := [ "category", "morphism", "nonneg_integer_or_infinity" ], - io_type := [ [ "mor", "n" ], [ "Ap", "mor_source" ] ], + input_arguments_names := [ "cat", "mor", "n" ], + output_range_getter_string := "Source( mor )", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "SimplifyRange_IsoFromInputObject", redirect_function := function( cat, alpha, n ) @@ -3401,7 +3817,9 @@ SimplifySource_IsoToInputObject := rec( SimplifySource_IsoFromInputObject := rec( filter_list := [ "category", "morphism", "nonneg_integer_or_infinity" ], - io_type := [ [ "mor", "n" ], [ "mor_source", "Ap" ] ], + input_arguments_names := [ "cat", "mor", "n" ], + output_source_getter_string := "Source( mor )", + output_source_getter_preconditions := [ ], return_type := "morphism", dual_operation := "SimplifyRange_IsoToInputObject", redirect_function := "SimplifySource_IsoToInputObject", @@ -3411,7 +3829,9 @@ SimplifySource_IsoFromInputObject := rec( ## SimplifyRange* SimplifyRange := rec( filter_list := [ "category", "morphism", "nonneg_integer_or_infinity" ], - io_type := [ [ "mor", "n" ], [ "mor_source", "Bp" ] ], + input_arguments_names := [ "cat", "mor", "n" ], + output_source_getter_string := "Source( mor )", + output_source_getter_preconditions := [ ], return_type := "morphism", dual_operation := "SimplifySource", redirect_function := "SimplifyObject", @@ -3420,7 +3840,9 @@ SimplifyRange := rec( SimplifyRange_IsoToInputObject := rec( filter_list := [ "category", "morphism", "nonneg_integer_or_infinity" ], - io_type := [ [ "mor", "n" ], [ "Bp", "mor_range" ] ], + input_arguments_names := [ "cat", "mor", "n" ], + output_range_getter_string := "Range( mor )", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "SimplifySource_IsoFromInputObject", redirect_function := function( cat, alpha, n ) @@ -3437,7 +3859,9 @@ SimplifyRange_IsoToInputObject := rec( SimplifyRange_IsoFromInputObject := rec( filter_list := [ "category", "morphism", "nonneg_integer_or_infinity" ], - io_type := [ [ "mor", "n" ], [ "mor_range", "Bp" ] ], + input_arguments_names := [ "cat", "mor", "n" ], + output_source_getter_string := "Range( mor )", + output_source_getter_preconditions := [ ], return_type := "morphism", dual_operation := "SimplifySource_IsoToInputObject", redirect_function := "SimplifySource_IsoToInputObject", @@ -3447,7 +3871,7 @@ SimplifyRange_IsoFromInputObject := rec( ## SimplifySourceAndRange* SimplifySourceAndRange := rec( filter_list := [ "category", "morphism", "nonneg_integer_or_infinity" ], - io_type := [ [ "mor", "n" ], [ "Ap", "Bp" ] ], + input_arguments_names := [ "cat", "mor", "n" ], return_type := "morphism", dual_operation := "SimplifySourceAndRange", redirect_function := "SimplifyObject", @@ -3456,7 +3880,9 @@ SimplifySourceAndRange := rec( SimplifySourceAndRange_IsoToInputSource := rec( filter_list := [ "category", "morphism", "nonneg_integer_or_infinity" ], - io_type := [ [ "mor", "n" ], [ "Ap", "mor_source" ] ], + input_arguments_names := [ "cat", "mor", "n" ], + output_range_getter_string := "Source( mor )", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "SimplifySourceAndRange_IsoFromInputRange", redirect_function := "SimplifySource_IsoToInputObject", @@ -3465,7 +3891,9 @@ SimplifySourceAndRange_IsoToInputSource := rec( SimplifySourceAndRange_IsoFromInputSource := rec( filter_list := [ "category", "morphism", "nonneg_integer_or_infinity" ], - io_type := [ [ "mor", "n" ], [ "mor_source", "Ap" ] ], + input_arguments_names := [ "cat", "mor", "n" ], + output_source_getter_string := "Source( mor )", + output_source_getter_preconditions := [ ], return_type := "morphism", dual_operation := "SimplifySourceAndRange_IsoToInputRange", redirect_function := "SimplifySource_IsoToInputObject", @@ -3474,7 +3902,9 @@ SimplifySourceAndRange_IsoFromInputSource := rec( SimplifySourceAndRange_IsoToInputRange := rec( filter_list := [ "category", "morphism", "nonneg_integer_or_infinity" ], - io_type := [ [ "mor", "n" ], [ "Bp", "mor_range" ] ], + input_arguments_names := [ "cat", "mor", "n" ], + output_range_getter_string := "Range( mor )", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "SimplifySourceAndRange_IsoFromInputSource", redirect_function := "SimplifySource_IsoToInputObject", @@ -3483,7 +3913,9 @@ SimplifySourceAndRange_IsoToInputRange := rec( SimplifySourceAndRange_IsoFromInputRange := rec( filter_list := [ "category", "morphism", "nonneg_integer_or_infinity" ], - io_type := [ [ "mor", "n" ], [ "mor_range", "Bp" ] ], + input_arguments_names := [ "cat", "mor", "n" ], + output_source_getter_string := "Range( mor )", + output_source_getter_preconditions := [ ], return_type := "morphism", dual_operation := "SimplifySourceAndRange_IsoToInputSource", redirect_function := "SimplifySource_IsoToInputObject", @@ -3493,7 +3925,7 @@ SimplifySourceAndRange_IsoFromInputRange := rec( ## SimplifyEndo* SimplifyEndo := rec( filter_list := [ "category", "morphism", "nonneg_integer_or_infinity" ], - io_type := [ [ "mor", "n" ], [ "Ap", "Ap" ] ], + input_arguments_names := [ "cat", "mor", "n" ], return_type := "morphism", dual_operation := "SimplifyEndo", redirect_function := "SimplifyObject", @@ -3514,7 +3946,9 @@ SimplifyEndo := rec( SimplifyEndo_IsoFromInputObject := rec( filter_list := [ "category", "morphism", "nonneg_integer_or_infinity" ], - io_type := [ [ "mor", "n" ], [ "mor_source", "Ap" ] ], + input_arguments_names := [ "cat", "mor", "n" ], + output_source_getter_string := "Source( mor )", + output_source_getter_preconditions := [ ], return_type := "morphism", dual_operation := "SimplifyEndo_IsoToInputObject", redirect_function := "SimplifySource_IsoToInputObject", @@ -3523,7 +3957,9 @@ SimplifyEndo_IsoFromInputObject := rec( SimplifyEndo_IsoToInputObject := rec( filter_list := [ "category", "morphism", "nonneg_integer_or_infinity" ], - io_type := [ [ "mor", "n" ], [ "Ap", "mor_range" ] ], + input_arguments_names := [ "cat", "mor", "n" ], + output_range_getter_string := "Range( mor )", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "SimplifyEndo_IsoFromInputObject", redirect_function := "SimplifySource_IsoToInputObject", @@ -3532,19 +3968,19 @@ SimplifyEndo_IsoToInputObject := rec( SomeReductionBySplitEpiSummand := rec( filter_list := [ "category", "morphism" ], - io_type := [ [ "alpha" ], [ "Ap", "Bp" ] ], + input_arguments_names := [ "cat", "alpha" ], return_type := "morphism", ), SomeReductionBySplitEpiSummand_MorphismToInputRange := rec( filter_list := [ "category", "morphism" ], - io_type := [ [ "alpha" ], [ "Bp", "B" ] ], + input_arguments_names := [ "cat", "alpha" ], return_type := "morphism", ), SomeReductionBySplitEpiSummand_MorphismFromInputRange := rec( filter_list := [ "category", "morphism" ], - io_type := [ [ "alpha" ], [ "B", "Bp" ] ], + input_arguments_names := [ "cat", "alpha" ], return_type := "morphism", ), @@ -3586,7 +4022,9 @@ ProjectiveCoverObject := rec( EpimorphismFromProjectiveCoverObject := rec( filter_list := [ "category", "object" ], - io_type := [ [ "A" ], [ "P", "A" ] ], + input_arguments_names := [ "cat", "A" ], + output_range_getter_string := "A", + output_range_getter_preconditions := [ ], with_given_object_position := "Source", return_type := "morphism", dual_operation := "MonomorphismIntoInjectiveEnvelopeObject", @@ -3594,7 +4032,11 @@ EpimorphismFromProjectiveCoverObject := rec( EpimorphismFromProjectiveCoverObjectWithGivenProjectiveCoverObject := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "A", "P" ], [ "P", "A" ] ], + input_arguments_names := [ "cat", "A", "P" ], + output_source_getter_string := "P", + output_source_getter_preconditions := [ ], + output_range_getter_string := "A", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "MonomorphismIntoInjectiveEnvelopeObjectWithGivenInjectiveEnvelopeObject", is_merely_set_theoretic := true ), @@ -3607,7 +4049,9 @@ InjectiveEnvelopeObject := rec( MonomorphismIntoInjectiveEnvelopeObject := rec( filter_list := [ "category", "object" ], - io_type := [ [ "A" ], [ "A", "I" ] ], + input_arguments_names := [ "cat", "A" ], + output_source_getter_string := "A", + output_source_getter_preconditions := [ ], with_given_object_position := "Range", return_type := "morphism", dual_operation := "EpimorphismFromProjectiveCoverObject", @@ -3615,7 +4059,11 @@ MonomorphismIntoInjectiveEnvelopeObject := rec( MonomorphismIntoInjectiveEnvelopeObjectWithGivenInjectiveEnvelopeObject := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "A", "I" ], [ "A", "I" ] ], + input_arguments_names := [ "cat", "A", "I" ], + output_source_getter_string := "A", + output_source_getter_preconditions := [ ], + output_range_getter_string := "I", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "EpimorphismFromProjectiveCoverObjectWithGivenProjectiveCoverObject", is_merely_set_theoretic := true ), @@ -3682,7 +4130,7 @@ rec( InstallGlobalFunction( "CAP_INTERNAL_ENHANCE_NAME_RECORD_LIMITS", function ( limits ) - local object_specification, morphism_specification, source_position, type, range_position, unbound_morphism_positions, number_of_unbound_morphisms, unbound_objects, morphism, unbound_object_positions, number_of_unbound_objects, targets, target_positions, nontarget_positions, number_of_targets, number_of_nontargets, diagram_filter_list, diagram_input_type, limit, position; + local object_specification, morphism_specification, source_position, type, range_position, unbound_morphism_positions, number_of_unbound_morphisms, unbound_objects, morphism, unbound_object_positions, number_of_unbound_objects, targets, target_positions, nontarget_positions, number_of_targets, number_of_nontargets, diagram_filter_list, diagram_arguments_names, limit, position; for limit in limits do object_specification := limit.object_specification; @@ -3799,30 +4247,30 @@ InstallGlobalFunction( "CAP_INTERNAL_ENHANCE_NAME_RECORD_LIMITS", limit.nontarget_positions := nontarget_positions; limit.number_of_nontargets := number_of_nontargets; - #### get filter list and input type of the diagram + #### get filter list and names of input arguments of the diagram diagram_filter_list := [ ]; - diagram_input_type := [ ]; + diagram_arguments_names := [ ]; if number_of_unbound_objects = 1 then Add( diagram_filter_list, "object" ); - Add( diagram_input_type, "X" ); + Add( diagram_arguments_names, "X" ); elif number_of_unbound_objects > 1 then Add( diagram_filter_list, "list_of_objects" ); - Add( diagram_input_type, "objects" ); + Add( diagram_arguments_names, "objects" ); fi; if number_of_unbound_morphisms = 1 then Add( diagram_filter_list, "morphism" ); - Add( diagram_input_type, "alpha" ); + Add( diagram_arguments_names, "alpha" ); elif number_of_unbound_morphisms > 1 then if number_of_targets = 1 then Add( diagram_filter_list, "object" ); - Add( diagram_input_type, "Y" ); + Add( diagram_arguments_names, "Y" ); fi; Add( diagram_filter_list, "list_of_morphisms" ); - Add( diagram_input_type, "morphisms" ); + Add( diagram_arguments_names, "morphisms" ); fi; limit.diagram_filter_list := diagram_filter_list; - limit.diagram_input_type := diagram_input_type; + limit.diagram_arguments_names := diagram_arguments_names; #### set default projection/injection/universal morphism names if number_of_targets > 0 and not IsBound( limit.limit_projection_name ) then @@ -3861,18 +4309,18 @@ InstallGlobalFunction( "CAP_INTERNAL_ENHANCE_NAME_RECORD_LIMITS", if Length( diagram_filter_list ) > 0 then if limit.number_of_targets = 1 then limit.diagram_morphism_filter_list := [ "morphism" ]; - limit.diagram_morphism_input_type := [ "mu" ]; + limit.diagram_morphism_arguments_names := [ "mu" ]; else limit.diagram_morphism_filter_list := [ "list_of_morphisms" ]; - limit.diagram_morphism_input_type := [ "L" ]; + limit.diagram_morphism_arguments_names := [ "L" ]; fi; else limit.diagram_morphism_filter_list := [ ]; - limit.diagram_morphism_input_type := [ ]; + limit.diagram_morphism_arguments_names := [ ]; fi; - limit.functorial_source_diagram_arguments_names := limit.diagram_input_type; - limit.functorial_range_diagram_arguments_names := List( limit.diagram_input_type, x -> Concatenation( x, "p" ) ); + limit.functorial_source_diagram_arguments_names := limit.diagram_arguments_names; + limit.functorial_range_diagram_arguments_names := List( limit.diagram_arguments_names, x -> Concatenation( x, "p" ) ); od; end ); @@ -3920,7 +4368,7 @@ end ); InstallGlobalFunction( CAP_INTERNAL_VALIDATE_LIMITS_IN_NAME_RECORD, function ( method_name_record, limits ) - local make_record_with_given, make_colimit, object_filter_list, object_input_arguments_names, projection_filter_list, projection_io_type, morphism_to_sink_filter_list, morphism_to_sink_io_type, universal_morphism_filter_list, universal_morphism_io_type, object_record, projection_record, morphism_to_sink_record, filter_list, io_type, with_given_object_position, return_type, dual_operation, universal_morphism_record, functorial_record, functorial_with_given_record, limit; + local make_record_with_given, make_colimit, object_filter_list, object_input_arguments_names, projection_filter_list, projection_input_arguments_names, projection_range_getter_string, morphism_to_sink_filter_list, morphism_to_sink_input_arguments_names, morphism_to_sink_range_getter_string, universal_morphism_filter_list, universal_morphism_input_arguments_names, object_record, projection_record, morphism_to_sink_record, universal_morphism_record, functorial_record, functorial_with_given_record, limit; #### helper functions make_record_with_given := function ( record, object_name, coobject_name ) @@ -3928,10 +4376,13 @@ InstallGlobalFunction( CAP_INTERNAL_VALIDATE_LIMITS_IN_NAME_RECORD, record.function_name := Concatenation( record.function_name, "WithGiven", object_name ); Add( record.filter_list, "object" ); + Add( record.input_arguments_names, "P" ); if record.with_given_object_position = "Source" then - Add( record.io_type[1], record.io_type[2][1] ); + record.output_source_getter_string := "P"; + record.output_source_getter_preconditions := [ ]; else - Add( record.io_type[1], record.io_type[2][2] ); + record.output_range_getter_string := "P"; + record.output_range_getter_preconditions := [ ]; fi; record.dual_operation := Concatenation( record.dual_operation, "WithGiven", coobject_name ); Unbind( record.with_given_object_position ); @@ -3940,7 +4391,7 @@ InstallGlobalFunction( CAP_INTERNAL_VALIDATE_LIMITS_IN_NAME_RECORD, end; make_colimit := function ( limit, record ) - local orig_function_name; + local orig_function_name, orig_output_source_getter_string, orig_output_source_getter_preconditions; record := StructuralCopy( record ); @@ -3948,14 +4399,6 @@ InstallGlobalFunction( CAP_INTERNAL_VALIDATE_LIMITS_IN_NAME_RECORD, record.function_name := record.dual_operation; record.dual_operation := orig_function_name; - # reverse the output type, except if the input is reversed - if IsBound( record.io_type ) and not (IsBound( record.dual_arguments_reversed ) and record.dual_arguments_reversed) then - record.io_type[2] := Reversed( record.io_type[2] ); - record.io_type[2] := List( record.io_type[2], x -> ReplacedString( x, "source", "tmp" ) ); - record.io_type[2] := List( record.io_type[2], x -> ReplacedString( x, "range", "source" ) ); - record.io_type[2] := List( record.io_type[2], x -> ReplacedString( x, "tmp", "range" ) ); - fi; - if IsBound( record.functorial ) then Assert( 0, record.functorial = limit.limit_functorial_name ); @@ -3971,29 +4414,77 @@ InstallGlobalFunction( CAP_INTERNAL_VALIDATE_LIMITS_IN_NAME_RECORD, record.with_given_object_position := "Source"; fi; fi; - - if IsBound( record.output_source_getter_string ) then - record.output_source_getter_string := ReplacedString( record.output_source_getter_string, limit.limit_object_name, limit.colimit_object_name ); + + # reverse output getters, except if the input is reversed + if not (IsBound( record.dual_arguments_reversed ) and record.dual_arguments_reversed) then + + orig_output_source_getter_string := fail; + + if IsBound( record.output_source_getter_string ) then + + orig_output_source_getter_string := record.output_source_getter_string; + orig_output_source_getter_preconditions := record.output_source_getter_preconditions; + + fi; + + if IsBound( record.output_range_getter_string ) then + + record.output_source_getter_string := record.output_range_getter_string; + record.output_source_getter_preconditions := record.output_range_getter_preconditions; + + else + + Unbind( record.output_source_getter_string ); + Unbind( record.output_source_getter_preconditions ); + + fi; + + if orig_output_source_getter_string <> fail then + + record.output_range_getter_string := orig_output_source_getter_string; + record.output_range_getter_preconditions := orig_output_source_getter_preconditions; + + else + + Unbind( record.output_range_getter_string ); + Unbind( record.output_range_getter_preconditions ); + + fi; + fi; - if IsBound( record.output_source_getter_preconditions ) then - if record.output_source_getter_preconditions = [ [ limit.limit_object_name, 1 ] ] then + if IsBound( record.output_source_getter_string ) then + + record.output_source_getter_string := ReplacedString( record.output_source_getter_string, "Source", "tmp" ); + record.output_source_getter_string := ReplacedString( record.output_source_getter_string, "Range", "Source" ); + record.output_source_getter_string := ReplacedString( record.output_source_getter_string, "tmp", "Range" ); + + if IsEmpty( record.output_source_getter_preconditions ) then + # do nothing + elif record.output_source_getter_preconditions = [ [ limit.limit_object_name, 1 ] ] then + record.output_source_getter_string := ReplacedString( record.output_source_getter_string, limit.limit_object_name, limit.colimit_object_name ); record.output_source_getter_preconditions := [ [ limit.colimit_object_name, 1 ] ]; else Error( "this case is not supported yet" ); fi; + fi; if IsBound( record.output_range_getter_string ) then - record.output_range_getter_string := ReplacedString( record.output_range_getter_string, limit.limit_object_name, limit.colimit_object_name ); - fi; - - if IsBound( record.output_range_getter_preconditions ) then - if record.output_range_getter_preconditions = [ [ limit.limit_object_name, 1 ] ] then + + record.output_range_getter_string := ReplacedString( record.output_range_getter_string, "Source", "tmp" ); + record.output_range_getter_string := ReplacedString( record.output_range_getter_string, "Range", "Source" ); + record.output_range_getter_string := ReplacedString( record.output_range_getter_string, "tmp", "Range" ); + + if IsEmpty( record.output_range_getter_preconditions ) then + # do nothing + elif record.output_range_getter_preconditions = [ [ limit.limit_object_name, 1 ] ] then + record.output_range_getter_string := ReplacedString( record.output_range_getter_string, limit.limit_object_name, limit.colimit_object_name ); record.output_range_getter_preconditions := [ [ limit.colimit_object_name, 1 ] ]; else Error( "this case is not supported yet" ); fi; + fi; return record; @@ -4003,39 +4494,39 @@ InstallGlobalFunction( CAP_INTERNAL_VALIDATE_LIMITS_IN_NAME_RECORD, #### get filter lists and io types object_filter_list := Concatenation( [ "category" ], StructuralCopy( limit.diagram_filter_list ) ); - object_input_arguments_names := Concatenation( [ "cat" ], limit.diagram_input_type ); + object_input_arguments_names := Concatenation( [ "cat" ], limit.diagram_arguments_names ); # only used if limit.number_of_targets > 0 projection_filter_list := Concatenation( [ "category" ], StructuralCopy( limit.diagram_filter_list ) ); - projection_io_type := [ StructuralCopy( limit.diagram_input_type ), [ ] ]; + projection_input_arguments_names := Concatenation( [ "cat" ], limit.diagram_arguments_names ); if limit.number_of_targets > 1 then Add( projection_filter_list, "integer" ); - Add( projection_io_type[1], "k" ); + Add( projection_input_arguments_names, "k" ); fi; if limit.target_positions = limit.unbound_object_positions then - # io_type can be derived from the objects + # range can be derived from the objects if limit.number_of_targets = 1 then - projection_io_type[2] := [ "P", "X" ]; + projection_range_getter_string := "X"; else - projection_io_type[2] := [ "P", "objects_k" ]; + projection_range_getter_string := "objects[k]"; fi; elif limit.target_positions = List( limit.unbound_morphism_positions, i -> limit.morphism_specification[i][1] ) then - # io_type can be derived from the morphisms as sources + # range can be derived from the morphisms as sources if limit.number_of_unbound_morphisms = 1 then - projection_io_type[2] := [ "P", "alpha_source" ]; + projection_range_getter_string := "Source( alpha )"; elif limit.number_of_targets = 1 then - projection_io_type[2] := [ "P", "Y" ]; + projection_range_getter_string := "Y"; else - projection_io_type[2] := [ "P", "morphisms_k_source" ]; + projection_range_getter_string := "Source( morphisms[k] )"; fi; elif limit.target_positions = List( limit.unbound_morphism_positions, i -> limit.morphism_specification[i][3] ) then - # io_type can be derived from the morphisms as ranges + # range can be derived from the morphisms as ranges if limit.number_of_unbound_morphisms = 1 then - projection_io_type[2] := [ "P", "alpha_range" ]; + projection_range_getter_string := "Range( alpha )"; elif limit.number_of_targets = 1 then - projection_io_type[2] := [ "P", "Y" ]; + projection_range_getter_string := "Y"; else - projection_io_type[2] := [ "P", "morphisms_k_range" ]; + projection_range_getter_string := "Range( morphisms[k] )"; fi; else Error( "Warning: cannot express io_type" ); @@ -4043,21 +4534,22 @@ InstallGlobalFunction( CAP_INTERNAL_VALIDATE_LIMITS_IN_NAME_RECORD, # only used if limit.number_of_nontargets = 1 morphism_to_sink_filter_list := Concatenation( [ "category" ], StructuralCopy( limit.diagram_filter_list ) ); - morphism_to_sink_io_type := [ StructuralCopy( limit.diagram_input_type ), [ ] ]; + morphism_to_sink_input_arguments_names := Concatenation( [ "cat" ], limit.diagram_arguments_names ); + morphism_to_sink_range_getter_string := [ StructuralCopy( limit.diagram_arguments_names ), [ ] ]; if limit.number_of_unbound_morphisms = 1 then - morphism_to_sink_io_type[2] := [ "P", "alpha_range" ]; + morphism_to_sink_range_getter_string := "Range( alpha )"; elif limit.number_of_unbound_morphisms > 1 then - morphism_to_sink_io_type[2] := [ "P", "morphisms_1_range" ]; + morphism_to_sink_range_getter_string := "Range( morphisms[1] )"; fi; universal_morphism_filter_list := Concatenation( [ "category" ], StructuralCopy( limit.diagram_filter_list ), [ "object" ] ); - universal_morphism_io_type := [ Concatenation( StructuralCopy( limit.diagram_input_type ), [ "T" ] ), [ "T", "P" ] ]; + universal_morphism_input_arguments_names := Concatenation( [ "cat" ], limit.diagram_arguments_names, [ "T" ] ); if limit.number_of_targets = 1 then Add( universal_morphism_filter_list, "morphism" ); - Add( universal_morphism_io_type[1], "tau" ); + Add( universal_morphism_input_arguments_names, "tau" ); elif limit.number_of_targets > 1 then Add( universal_morphism_filter_list, "list_of_morphisms" ); - Add( universal_morphism_io_type[1], "tau" ); + Add( universal_morphism_input_arguments_names, "tau" ); fi; @@ -4075,9 +4567,11 @@ InstallGlobalFunction( CAP_INTERNAL_VALIDATE_LIMITS_IN_NAME_RECORD, projection_record := rec( function_name := limit.limit_projection_name, filter_list := projection_filter_list, - io_type := projection_io_type, - with_given_object_position := "Source", + input_arguments_names := projection_input_arguments_names, return_type := "morphism", + output_range_getter_string := projection_range_getter_string, + output_range_getter_preconditions := [ ], + with_given_object_position := "Source", dual_operation := limit.colimit_injection_name, ); fi; @@ -4086,9 +4580,11 @@ InstallGlobalFunction( CAP_INTERNAL_VALIDATE_LIMITS_IN_NAME_RECORD, morphism_to_sink_record := rec( function_name := Concatenation( "MorphismFrom", limit.limit_object_name, "ToSink" ), filter_list := morphism_to_sink_filter_list, - io_type := morphism_to_sink_io_type, - with_given_object_position := "Source", + input_arguments_names := morphism_to_sink_input_arguments_names, return_type := "morphism", + output_range_getter_string := morphism_to_sink_range_getter_string, + output_range_getter_preconditions := [ ], + with_given_object_position := "Source", dual_operation := limit.colimit_morphism_from_source_name, ); fi; @@ -4096,16 +4592,18 @@ InstallGlobalFunction( CAP_INTERNAL_VALIDATE_LIMITS_IN_NAME_RECORD, universal_morphism_record := rec( function_name := limit.limit_universal_morphism_name, filter_list := universal_morphism_filter_list, - io_type := universal_morphism_io_type, - with_given_object_position := "Range", + input_arguments_names := universal_morphism_input_arguments_names, return_type := "morphism", + output_source_getter_string := "T", + output_source_getter_preconditions := [ ], + with_given_object_position := "Range", dual_operation := limit.colimit_universal_morphism_name, ); functorial_record := rec( function_name := limit.limit_functorial_name, filter_list := Concatenation( [ "category" ], limit.diagram_filter_list, limit.diagram_morphism_filter_list, limit.diagram_filter_list ), - input_arguments_names := Concatenation( [ "cat" ], limit.functorial_source_diagram_arguments_names, limit.diagram_morphism_input_type, limit.functorial_range_diagram_arguments_names ), + input_arguments_names := Concatenation( [ "cat" ], limit.functorial_source_diagram_arguments_names, limit.diagram_morphism_arguments_names, limit.functorial_range_diagram_arguments_names ), return_type := "morphism", # object_name output_source_getter_string := ReplacedStringViaRecord( @@ -4126,8 +4624,12 @@ InstallGlobalFunction( CAP_INTERNAL_VALIDATE_LIMITS_IN_NAME_RECORD, functorial_with_given_record := rec( function_name := limit.limit_functorial_with_given_name, filter_list := Concatenation( [ "category", "object" ], limit.diagram_filter_list, limit.diagram_morphism_filter_list, limit.diagram_filter_list, [ "object" ] ), - io_type := [ Concatenation( [ "P" ], limit.functorial_source_diagram_arguments_names, limit.diagram_morphism_input_type, limit.functorial_range_diagram_arguments_names, [ "Pp" ] ), [ "P", "Pp" ] ], + input_arguments_names := Concatenation( [ "cat", "P" ], limit.functorial_source_diagram_arguments_names, limit.diagram_morphism_arguments_names, limit.functorial_range_diagram_arguments_names, [ "Pp" ] ), return_type := "morphism", + output_source_getter_string := "P", + output_source_getter_preconditions := [ ], + output_range_getter_string := "Pp", + output_range_getter_preconditions := [ ], dual_operation := limit.colimit_functorial_with_given_name, dual_arguments_reversed := true, ); diff --git a/CartesianCategories/PackageInfo.g b/CartesianCategories/PackageInfo.g index 483996d4d9..b57fc811ee 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.06-01", +Version := "2023.07-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", diff --git a/CartesianCategories/gap/BraidedCartesianCategoriesMethodRecord.gi b/CartesianCategories/gap/BraidedCartesianCategoriesMethodRecord.gi index 9f582f5e6a..6d84c67a30 100644 --- a/CartesianCategories/gap/BraidedCartesianCategoriesMethodRecord.gi +++ b/CartesianCategories/gap/BraidedCartesianCategoriesMethodRecord.gi @@ -8,7 +8,7 @@ InstallValue( BRAIDED_CARTESIAN_CATEGORIES_METHOD_NAME_RECORD, rec( CartesianBraiding := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "a", "b" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "a", "b" ], output_source_getter_string := "BinaryDirectProduct( cat, a, b )", output_source_getter_preconditions := [ [ "DirectProduct", 1 ] ], output_range_getter_string := "BinaryDirectProduct( cat, b, a )", @@ -21,7 +21,11 @@ CartesianBraiding := rec( CartesianBraidingWithGivenDirectProducts := rec( filter_list := [ "category", "object", "object", "object", "object" ], - io_type := [ [ "s", "a", "b", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "a", "b", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "CocartesianBraidingInverseWithGivenCoproducts", dual_with_given_objects_reversed := true, @@ -29,7 +33,7 @@ CartesianBraidingWithGivenDirectProducts := rec( CartesianBraidingInverse := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "a", "b" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "a", "b" ], output_source_getter_string := "BinaryDirectProduct( cat, b, a )", output_source_getter_preconditions := [ [ "DirectProduct", 1 ] ], output_range_getter_string := "BinaryDirectProduct( cat, a, b )", @@ -42,7 +46,11 @@ CartesianBraidingInverse := rec( CartesianBraidingInverseWithGivenDirectProducts := rec( filter_list := [ "category", "object", "object", "object", "object" ], - io_type := [ [ "s", "a", "b", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "a", "b", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "CocartesianBraidingWithGivenCoproducts", dual_with_given_objects_reversed := true, diff --git a/CartesianCategories/gap/BraidedCocartesianCategoriesMethodRecord.gi b/CartesianCategories/gap/BraidedCocartesianCategoriesMethodRecord.gi index 28aba2f40c..e0a7e0069c 100644 --- a/CartesianCategories/gap/BraidedCocartesianCategoriesMethodRecord.gi +++ b/CartesianCategories/gap/BraidedCocartesianCategoriesMethodRecord.gi @@ -8,7 +8,7 @@ InstallValue( BRAIDED_COCARTESIAN_CATEGORIES_METHOD_NAME_RECORD, rec( CocartesianBraiding := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "a", "b" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "a", "b" ], output_source_getter_string := "BinaryCoproduct( cat, a, b )", output_source_getter_preconditions := [ [ "Coproduct", 1 ] ], output_range_getter_string := "BinaryCoproduct( cat, b, a )", @@ -21,7 +21,11 @@ CocartesianBraiding := rec( CocartesianBraidingWithGivenCoproducts := rec( filter_list := [ "category", "object", "object", "object", "object" ], - io_type := [ [ "s", "a", "b", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "a", "b", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "CartesianBraidingInverseWithGivenDirectProducts", dual_with_given_objects_reversed := true, @@ -29,7 +33,7 @@ CocartesianBraidingWithGivenCoproducts := rec( CocartesianBraidingInverse := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "a", "b" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "a", "b" ], output_source_getter_string := "BinaryCoproduct( cat, b, a )", output_source_getter_preconditions := [ [ "Coproduct", 1 ] ], output_range_getter_string := "BinaryCoproduct( cat, a, b )", @@ -42,7 +46,11 @@ CocartesianBraidingInverse := rec( CocartesianBraidingInverseWithGivenCoproducts := rec( filter_list := [ "category", "object", "object", "object", "object" ], - io_type := [ [ "s", "a", "b", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "a", "b", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "CartesianBraidingWithGivenDirectProducts", dual_with_given_objects_reversed := true, diff --git a/CartesianCategories/gap/CartesianCategoriesMethodRecord.gi b/CartesianCategories/gap/CartesianCategoriesMethodRecord.gi index 35f55e7bdf..bf15bd5ddc 100644 --- a/CartesianCategories/gap/CartesianCategoriesMethodRecord.gi +++ b/CartesianCategories/gap/CartesianCategoriesMethodRecord.gi @@ -10,7 +10,9 @@ InstallValue( CARTESIAN_CATEGORIES_METHOD_NAME_RECORD, rec( CartesianDiagonal := rec( filter_list := [ "category", "object", "integer" ], - io_type := [ [ "a", "n" ], [ "a", "cartesian_power" ] ], + input_arguments_names := [ "cat", "a", "n" ], + output_source_getter_string := "a", + output_source_getter_preconditions := [ ], output_source_getter_string := "a", output_range_getter_string := "DirectProduct( cat, ListWithIdenticalEntries( n, a ) )", output_range_getter_preconditions := [ [ "DirectProduct", 1 ] ], @@ -21,7 +23,9 @@ CartesianDiagonal := rec( CartesianDiagonalWithGivenCartesianPower := rec( filter_list := [ "category", "object", "integer", "object" ], - io_type := [ [ "a", "n", "cartesian_power" ], [ "a", "cartesian_power" ] ], + input_arguments_names := [ "cat", "a", "n", "cartesian_power" ], + output_source_getter_string := "a", + output_source_getter_preconditions := [ ], output_source_getter_string := "a", output_range_getter_string := "cartesian_power", return_type := "morphism", @@ -31,7 +35,7 @@ CartesianDiagonalWithGivenCartesianPower := rec( DirectProductOnMorphisms := rec( filter_list := [ "category", "morphism", "morphism" ], - io_type := [ [ "alpha", "beta" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "alpha", "beta" ], output_source_getter_string := "BinaryDirectProduct( cat, Source( alpha ), Source( beta ) )", output_source_getter_preconditions := [ [ "DirectProduct", 1 ] ], output_range_getter_string := "BinaryDirectProduct( cat, Range( alpha ), Range( beta ) )", @@ -44,7 +48,11 @@ DirectProductOnMorphisms := rec( DirectProductOnMorphismsWithGivenDirectProducts := rec( filter_list := [ "category", "object", "morphism", "morphism", "object" ], - io_type := [ [ "s", "alpha", "beta", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "alpha", "beta", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "CoproductOnMorphismsWithGivenCoproducts", dual_with_given_objects_reversed := true, @@ -52,7 +60,7 @@ DirectProductOnMorphismsWithGivenDirectProducts := rec( CartesianAssociatorRightToLeft := rec( filter_list := [ "category", "object", "object", "object" ], - io_type := [ [ "a", "b", "c" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "a", "b", "c" ], output_source_getter_string := "BinaryDirectProduct( cat, a, BinaryDirectProduct( cat, b, c ) )", output_source_getter_preconditions := [ [ "DirectProduct", 2 ] ], output_range_getter_string := "BinaryDirectProduct( cat, BinaryDirectProduct( cat, a, b ), c )", @@ -65,7 +73,11 @@ CartesianAssociatorRightToLeft := rec( CartesianAssociatorRightToLeftWithGivenDirectProducts := rec( filter_list := [ "category", "object", "object", "object", "object", "object" ], - io_type := [ [ "s", "a", "b", "c", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "a", "b", "c", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "CocartesianAssociatorLeftToRightWithGivenCoproducts", dual_with_given_objects_reversed := true, @@ -73,7 +85,7 @@ CartesianAssociatorRightToLeftWithGivenDirectProducts := rec( CartesianAssociatorLeftToRight := rec( filter_list := [ "category", "object", "object", "object" ], - io_type := [ [ "a", "b", "c" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "a", "b", "c" ], output_source_getter_string := "BinaryDirectProduct( cat, BinaryDirectProduct( cat, a, b ), c )", output_source_getter_preconditions := [ [ "DirectProduct", 2 ] ], output_range_getter_string := "BinaryDirectProduct( cat, a, BinaryDirectProduct( cat, b, c ) )", @@ -86,7 +98,11 @@ CartesianAssociatorLeftToRight := rec( CartesianAssociatorLeftToRightWithGivenDirectProducts := rec( filter_list := [ "category", "object", "object", "object", "object", "object" ], - io_type := [ [ "s", "a", "b", "c", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "a", "b", "c", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "CocartesianAssociatorRightToLeftWithGivenCoproducts", dual_with_given_objects_reversed := true, @@ -94,7 +110,9 @@ CartesianAssociatorLeftToRightWithGivenDirectProducts := rec( CartesianLeftUnitor := rec( filter_list := [ "category", "object" ], - io_type := [ [ "a" ], [ "s", "a" ] ], + input_arguments_names := [ "cat", "a" ], + output_range_getter_string := "a", + output_range_getter_preconditions := [ ], output_source_getter_string := "BinaryDirectProduct( cat, TerminalObject( cat ), a )", output_source_getter_preconditions := [ [ "TerminalObject", 1 ], [ "DirectProduct", 1 ] ], output_range_getter_string := "a", @@ -105,7 +123,11 @@ CartesianLeftUnitor := rec( CartesianLeftUnitorWithGivenDirectProduct := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "a", "s" ], [ "s", "a" ] ], + input_arguments_names := [ "cat", "a", "s" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "a", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "CocartesianLeftUnitorInverseWithGivenCoproduct", dual_arguments_reversed := false, @@ -113,7 +135,9 @@ CartesianLeftUnitorWithGivenDirectProduct := rec( CartesianLeftUnitorInverse := rec( filter_list := [ "category", "object" ], - io_type := [ [ "a" ], [ "a", "r" ] ], + input_arguments_names := [ "cat", "a" ], + output_source_getter_string := "a", + output_source_getter_preconditions := [ ], output_source_getter_string := "a", output_range_getter_string := "BinaryDirectProduct( cat, TerminalObject( cat ), a )", output_range_getter_preconditions := [ [ "TerminalObject", 1 ], [ "DirectProduct", 1 ] ], @@ -124,7 +148,11 @@ CartesianLeftUnitorInverse := rec( CartesianLeftUnitorInverseWithGivenDirectProduct := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "a", "r" ], [ "a", "r" ] ], + input_arguments_names := [ "cat", "a", "r" ], + output_source_getter_string := "a", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "CocartesianLeftUnitorWithGivenCoproduct", dual_arguments_reversed := false, @@ -132,7 +160,9 @@ CartesianLeftUnitorInverseWithGivenDirectProduct := rec( CartesianRightUnitor := rec( filter_list := [ "category", "object" ], - io_type := [ [ "a" ], [ "s", "a" ] ], + input_arguments_names := [ "cat", "a" ], + output_range_getter_string := "a", + output_range_getter_preconditions := [ ], output_source_getter_string := "BinaryDirectProduct( cat, a, TerminalObject( cat ) )", output_source_getter_preconditions := [ [ "TerminalObject", 1 ], [ "DirectProduct", 1 ] ], output_range_getter_string := "a", @@ -143,7 +173,11 @@ CartesianRightUnitor := rec( CartesianRightUnitorWithGivenDirectProduct := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "a", "s" ], [ "s", "a" ] ], + input_arguments_names := [ "cat", "a", "s" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "a", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "CocartesianRightUnitorInverseWithGivenCoproduct", dual_arguments_reversed := false, @@ -151,7 +185,9 @@ CartesianRightUnitorWithGivenDirectProduct := rec( CartesianRightUnitorInverse := rec( filter_list := [ "category", "object" ], - io_type := [ [ "a" ], [ "a", "r" ] ], + input_arguments_names := [ "cat", "a" ], + output_source_getter_string := "a", + output_source_getter_preconditions := [ ], output_source_getter_string := "a", output_range_getter_string := "BinaryDirectProduct( cat, a, TerminalObject( cat ) )", output_range_getter_preconditions := [ [ "TerminalObject", 1 ], [ "DirectProduct", 1 ] ], @@ -162,7 +198,11 @@ CartesianRightUnitorInverse := rec( CartesianRightUnitorInverseWithGivenDirectProduct := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "a", "r" ], [ "a", "r" ] ], + input_arguments_names := [ "cat", "a", "r" ], + output_source_getter_string := "a", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "CocartesianRightUnitorWithGivenCoproduct", dual_arguments_reversed := false, diff --git a/CartesianCategories/gap/CartesianClosedCategoriesMethodRecord.gi b/CartesianCategories/gap/CartesianClosedCategoriesMethodRecord.gi index 28b2540016..4baff84bd3 100644 --- a/CartesianCategories/gap/CartesianClosedCategoriesMethodRecord.gi +++ b/CartesianCategories/gap/CartesianClosedCategoriesMethodRecord.gi @@ -20,7 +20,7 @@ ExponentialOnObjects := rec( ExponentialOnMorphisms := rec( filter_list := [ "category", "morphism", "morphism" ], - io_type := [ [ "alpha", "beta" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "alpha", "beta" ], output_source_getter_string := "ExponentialOnObjects( cat, Range( alpha ), Source( beta ) )", output_source_getter_preconditions := [ [ "ExponentialOnObjects", 1 ] ], output_range_getter_string := "ExponentialOnObjects( cat, Source( alpha ), Range( beta ) )", @@ -34,7 +34,11 @@ ExponentialOnMorphisms := rec( ExponentialOnMorphismsWithGivenExponentials := rec( filter_list := [ "category", "object", "morphism", "morphism", "object" ], - io_type := [ [ "s", "alpha", "beta", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "alpha", "beta", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "CoexponentialOnMorphismsWithGivenCoexponentials", dual_arguments_reversed := true, @@ -42,7 +46,9 @@ ExponentialOnMorphismsWithGivenExponentials := rec( CartesianEvaluationMorphism := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "a", "b" ], [ "s", "b" ] ], + input_arguments_names := [ "cat", "a", "b" ], + output_range_getter_string := "b", + output_range_getter_preconditions := [ ], output_source_getter_string := "BinaryDirectProduct( cat, ExponentialOnObjects( cat, a, b ), a )", output_source_getter_preconditions := [ [ "DirectProduct", 1 ], [ "ExponentialOnObjects", 1 ] ], output_range_getter_string := "b", @@ -55,7 +61,11 @@ CartesianEvaluationMorphism := rec( CartesianEvaluationMorphismWithGivenSource := rec( filter_list := [ "category", "object", "object", "object" ], - io_type := [ [ "a", "b", "s" ], [ "s", "b" ] ], + input_arguments_names := [ "cat", "a", "b", "s" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "b", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "CocartesianEvaluationMorphismWithGivenRange", dual_preprocessor_func := { cat, a, b, s } -> NTuple( 4, Opposite( cat ), Opposite( b ), Opposite( a ), Opposite( s ) ), @@ -64,7 +74,9 @@ CartesianEvaluationMorphismWithGivenSource := rec( CartesianCoevaluationMorphism := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "a", "b" ], [ "a", "r" ] ], + input_arguments_names := [ "cat", "a", "b" ], + output_source_getter_string := "a", + output_source_getter_preconditions := [ ], output_source_getter_string := "a", output_range_getter_string := "ExponentialOnObjects( cat, b, BinaryDirectProduct( cat, a, b ) )", output_range_getter_preconditions := [ [ "ExponentialOnObjects", 1 ], [ "DirectProduct", 1 ] ], @@ -77,7 +89,11 @@ CartesianCoevaluationMorphism := rec( CartesianCoevaluationMorphismWithGivenRange := rec( filter_list := [ "category", "object", "object", "object" ], - io_type := [ [ "a", "b", "r" ], [ "a", "r" ] ], + input_arguments_names := [ "cat", "a", "b", "r" ], + output_source_getter_string := "a", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "CocartesianCoevaluationMorphismWithGivenSource", dual_arguments_reversed := false, @@ -85,7 +101,9 @@ CartesianCoevaluationMorphismWithGivenRange := rec( DirectProductToExponentialAdjunctionMap := rec( filter_list := [ "category", "object", "object", "morphism" ], - io_type := [ [ "a", "b", "f" ], [ "a", "i" ] ], + input_arguments_names := [ "cat", "a", "b", "f" ], + output_source_getter_string := "a", + output_source_getter_preconditions := [ ], return_type := "morphism", dual_operation := "CoproductToCoexponentialAdjunctionMap", dual_arguments_reversed := false, @@ -94,7 +112,11 @@ DirectProductToExponentialAdjunctionMap := rec( DirectProductToExponentialAdjunctionMapWithGivenExponential := rec( filter_list := [ "category", "object", "object", "morphism", "object" ], - io_type := [ [ "a", "b", "f", "i" ], [ "a", "i" ] ], + input_arguments_names := [ "cat", "a", "b", "f", "i" ], + output_source_getter_string := "a", + output_source_getter_preconditions := [ ], + output_range_getter_string := "i", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "CoproductToCoexponentialAdjunctionMapWithGivenCoexponential", dual_arguments_reversed := false, @@ -102,7 +124,9 @@ DirectProductToExponentialAdjunctionMapWithGivenExponential := rec( ExponentialToDirectProductAdjunctionMap := rec( filter_list := [ "category", "object", "object", "morphism" ], - io_type := [ [ "b", "c", "g" ], [ "t", "c" ] ], + input_arguments_names := [ "cat", "b", "c", "g" ], + output_range_getter_string := "c", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "CoexponentialToCoproductAdjunctionMap", dual_preprocessor_func := { cat, a, b, g } -> NTuple( 4, Opposite( cat ), Opposite( b ), Opposite( a ), Opposite( g ) ), @@ -112,7 +136,11 @@ ExponentialToDirectProductAdjunctionMap := rec( ExponentialToDirectProductAdjunctionMapWithGivenDirectProduct := rec( filter_list := [ "category", "object", "object", "morphism", "object" ], - io_type := [ [ "b", "c", "g", "t" ], [ "t", "c" ] ], + input_arguments_names := [ "cat", "b", "c", "g", "t" ], + output_source_getter_string := "t", + output_source_getter_preconditions := [ ], + output_range_getter_string := "c", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "CoexponentialToCoproductAdjunctionMapWithGivenCoproduct", dual_preprocessor_func := { cat, a, b, g, t } -> NTuple( 4, Opposite( cat ), Opposite( b ), Opposite( a ), Opposite( g ),Opposite( t ) ), @@ -121,7 +149,7 @@ ExponentialToDirectProductAdjunctionMapWithGivenDirectProduct := rec( CartesianPreComposeMorphism := rec( filter_list := [ "category", "object", "object", "object" ], - io_type := [ [ "a", "b", "c" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "a", "b", "c" ], output_source_getter_string := "BinaryDirectProduct( cat, ExponentialOnObjects( cat, a, b ), ExponentialOnObjects( cat, b, c ) )", output_source_getter_preconditions := [ [ "DirectProduct", 1 ], [ "ExponentialOnObjects", 2 ] ], output_range_getter_string := "ExponentialOnObjects( cat, a, c )", @@ -135,7 +163,11 @@ CartesianPreComposeMorphism := rec( CartesianPreComposeMorphismWithGivenObjects := rec( filter_list := [ "category", "object", "object", "object", "object", "object" ], - io_type := [ [ "s", "a", "b", "c", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "a", "b", "c", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "CocartesianPreCoComposeMorphismWithGivenObjects", dual_arguments_reversed := true, @@ -143,7 +175,7 @@ CartesianPreComposeMorphismWithGivenObjects := rec( CartesianPostComposeMorphism := rec( filter_list := [ "category", "object", "object", "object" ], - io_type := [ [ "a", "b", "c" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "a", "b", "c" ], output_source_getter_string := "BinaryDirectProduct( cat, ExponentialOnObjects( cat, b, c ), ExponentialOnObjects( cat, a, b ) )", output_source_getter_preconditions := [ [ "DirectProduct", 1 ], [ "ExponentialOnObjects", 2 ] ], output_range_getter_string := "ExponentialOnObjects( cat, a, c )", @@ -157,7 +189,11 @@ CartesianPostComposeMorphism := rec( CartesianPostComposeMorphismWithGivenObjects := rec( filter_list := [ "category", "object", "object", "object", "object", "object" ], - io_type := [ [ "s", "a", "b", "c", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "a", "b", "c", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "CocartesianPostCoComposeMorphismWithGivenObjects", dual_arguments_reversed := true, @@ -173,7 +209,7 @@ CartesianDualOnObjects := rec( CartesianDualOnMorphisms := rec( filter_list := [ "category", "morphism" ], - io_type := [ [ "alpha" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "alpha" ], output_source_getter_string := "CartesianDualOnObjects( cat, Range( alpha ) )", output_source_getter_preconditions := [ [ "CartesianDualOnObjects", 1 ] ], output_range_getter_string := "CartesianDualOnObjects( cat, Source( alpha ) )", @@ -186,7 +222,11 @@ CartesianDualOnMorphisms := rec( CartesianDualOnMorphismsWithGivenCartesianDuals := rec( filter_list := [ "category", "object", "morphism", "object" ], - io_type := [ [ "s", "alpha", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "alpha", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "CocartesianDualOnMorphismsWithGivenCocartesianDuals", dual_arguments_reversed := true, @@ -194,7 +234,7 @@ CartesianDualOnMorphismsWithGivenCartesianDuals := rec( CartesianEvaluationForCartesianDual := rec( filter_list := [ "category", "object" ], - io_type := [ [ "a" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "a" ], output_source_getter_string := "BinaryDirectProduct( cat, CartesianDualOnObjects( cat, a ), a )", output_source_getter_preconditions := [ [ "DirectProduct", 1 ], [ "CartesianDualOnObjects", 1 ] ], output_range_getter_string := "TerminalObject( cat )", @@ -207,7 +247,11 @@ CartesianEvaluationForCartesianDual := rec( CartesianEvaluationForCartesianDualWithGivenDirectProduct := rec( filter_list := [ "category", "object", "object", "object" ], - io_type := [ [ "s", "a", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "a", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "CocartesianEvaluationForCocartesianDualWithGivenCoproduct", dual_arguments_reversed := true, @@ -215,7 +259,9 @@ CartesianEvaluationForCartesianDualWithGivenDirectProduct := rec( MorphismToCartesianBidual := rec( filter_list := [ "category", "object" ], - io_type := [ [ "a" ], [ "a", "r" ] ], + input_arguments_names := [ "cat", "a" ], + output_source_getter_string := "a", + output_source_getter_preconditions := [ ], output_source_getter_string := "a", output_range_getter_string := "CartesianDualOnObjects( cat, CartesianDualOnObjects( cat, a ) )", output_range_getter_preconditions := [ [ "CartesianDualOnObjects", 2 ] ], @@ -227,7 +273,11 @@ MorphismToCartesianBidual := rec( MorphismToCartesianBidualWithGivenCartesianBidual := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "a", "r" ], [ "a", "r" ] ], + input_arguments_names := [ "cat", "a", "r" ], + output_source_getter_string := "a", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "MorphismFromCocartesianBidualWithGivenCocartesianBidual", dual_arguments_reversed := false, @@ -262,7 +312,7 @@ DirectProductExponentialCompatibilityMorphismWithGivenObjects := rec( DirectProductCartesianDualityCompatibilityMorphism := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "a", "b" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "a", "b" ], output_source_getter_string := "BinaryDirectProduct( cat, CartesianDualOnObjects( cat, a ), CartesianDualOnObjects( cat, b ) )", output_source_getter_preconditions := [ [ "DirectProduct", 1 ], [ "CartesianDualOnObjects", 2 ] ], output_range_getter_string := "CartesianDualOnObjects( cat, BinaryDirectProduct( cat, a, b ) )", @@ -276,7 +326,11 @@ DirectProductCartesianDualityCompatibilityMorphism := rec( DirectProductCartesianDualityCompatibilityMorphismWithGivenObjects := rec( filter_list := [ "category", "object", "object", "object", "object" ], - io_type := [ [ "s", "a", "b", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "a", "b", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "CocartesianDualityCoproductCompatibilityMorphismWithGivenObjects", dual_with_given_objects_reversed := true, @@ -284,7 +338,7 @@ DirectProductCartesianDualityCompatibilityMorphismWithGivenObjects := rec( MorphismFromDirectProductToExponential := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "a", "b" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "a", "b" ], output_source_getter_string := "BinaryDirectProduct( cat, CartesianDualOnObjects( cat, a ), b )", output_source_getter_preconditions := [ [ "DirectProduct", 1 ], [ "CartesianDualOnObjects", 1 ] ], output_range_getter_string := "ExponentialOnObjects( cat, a, b )", @@ -298,7 +352,11 @@ MorphismFromDirectProductToExponential := rec( MorphismFromDirectProductToExponentialWithGivenObjects := rec( filter_list := [ "category", "object", "object", "object", "object" ], - io_type := [ [ "s", "a", "b", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "a", "b", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "MorphismFromCoexponentialToCoproductWithGivenObjects", dual_arguments_reversed := true, @@ -306,7 +364,7 @@ MorphismFromDirectProductToExponentialWithGivenObjects := rec( IsomorphismFromExponentialIntoTerminalObjectToCartesianDualObject := rec( filter_list := [ "category", "object" ], - io_type := [ [ "a" ], [ "i", "d" ] ], + input_arguments_names := [ "cat", "a" ], output_source_getter_string := "ExponentialOnObjects( cat, a, TerminalObject( cat ) )", output_source_getter_preconditions := [ [ "ExponentialOnObjects", 1 ], [ "TerminalObject", 1 ] ], output_range_getter_string := "CartesianDualOnObjects( cat, a )", @@ -318,7 +376,7 @@ IsomorphismFromExponentialIntoTerminalObjectToCartesianDualObject := rec( IsomorphismFromCartesianDualObjectToExponentialIntoTerminalObject := rec( filter_list := [ "category", "object" ], - io_type := [ [ "a" ], [ "d", "i" ] ], + input_arguments_names := [ "cat", "a" ], output_source_getter_string := "CartesianDualOnObjects( cat, a )", output_source_getter_preconditions := [ [ "CartesianDualOnObjects", 1 ] ], output_range_getter_string := "ExponentialOnObjects( cat, a, TerminalObject( cat ) )", @@ -330,7 +388,9 @@ IsomorphismFromCartesianDualObjectToExponentialIntoTerminalObject := rec( UniversalPropertyOfCartesianDual := rec( filter_list := [ "category", "object", "object", "morphism" ], - io_type := [ [ "t", "a", "alpha" ], [ "t", "d" ] ], + input_arguments_names := [ "cat", "t", "a", "alpha" ], + output_source_getter_string := "t", + output_source_getter_preconditions := [ ], return_type := "morphism", dual_operation := "UniversalPropertyOfCocartesianDual", dual_arguments_reversed := false, @@ -339,7 +399,7 @@ UniversalPropertyOfCartesianDual := rec( CartesianLambdaIntroduction := rec( filter_list := [ "category", "morphism" ], - io_type := [ [ "alpha" ], [ "u", "i" ] ], + input_arguments_names := [ "cat", "alpha" ], return_type := "morphism", dual_operation := "CocartesianLambdaIntroduction", # Test in CartesianClosedCategoriesTest @@ -347,7 +407,11 @@ CartesianLambdaIntroduction := rec( CartesianLambdaElimination := rec( filter_list := [ "category", "object", "object", "morphism" ], - io_type := [ [ "a", "b", "alpha" ], [ "a", "b" ] ], + input_arguments_names := [ "cat", "a", "b", "alpha" ], + output_source_getter_string := "a", + output_source_getter_preconditions := [ ], + output_range_getter_string := "b", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "CocartesianLambdaElimination", dual_preprocessor_func := { cat, a, b, alpha } -> NTuple( 4, Opposite( cat ), Opposite( b ), Opposite( a ), Opposite( alpha ) ), @@ -357,7 +421,9 @@ CartesianLambdaElimination := rec( IsomorphismFromObjectToExponential := rec( filter_list := [ "category", "object" ], - io_type := [ [ "a" ], [ "a", "r" ] ], + input_arguments_names := [ "cat", "a" ], + output_source_getter_string := "a", + output_source_getter_preconditions := [ ], output_source_getter_string := "a", output_range_getter_string := "ExponentialOnObjects( cat, TerminalObject( cat ), a )", output_range_getter_preconditions := [ [ "ExponentialOnObjects", 1 ], [ "TerminalObject", 1 ] ], @@ -369,7 +435,11 @@ IsomorphismFromObjectToExponential := rec( IsomorphismFromObjectToExponentialWithGivenExponential := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "a", "r" ], [ "a", "r" ] ], + input_arguments_names := [ "cat", "a", "r" ], + output_source_getter_string := "a", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "IsomorphismFromCoexponentialToObjectWithGivenCoexponential", dual_arguments_reversed := false, @@ -377,7 +447,9 @@ IsomorphismFromObjectToExponentialWithGivenExponential := rec( IsomorphismFromExponentialToObject := rec( filter_list := [ "category", "object" ], - io_type := [ [ "a" ], [ "s", "a" ] ], + input_arguments_names := [ "cat", "a" ], + output_range_getter_string := "a", + output_range_getter_preconditions := [ ], output_source_getter_string := "ExponentialOnObjects( cat, TerminalObject( cat ), a )", output_source_getter_preconditions := [ [ "ExponentialOnObjects", 1 ], [ "TerminalObject", 1 ] ], output_range_getter_string := "a", @@ -389,7 +461,11 @@ IsomorphismFromExponentialToObject := rec( IsomorphismFromExponentialToObjectWithGivenExponential := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "a", "s" ], [ "s", "a" ] ], + input_arguments_names := [ "cat", "a", "s" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "a", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "IsomorphismFromObjectToCoexponentialWithGivenCoexponential", dual_arguments_reversed := false, diff --git a/CartesianCategories/gap/CocartesianCategoriesMethodRecord.gi b/CartesianCategories/gap/CocartesianCategoriesMethodRecord.gi index f7c7553157..5a217f90ef 100644 --- a/CartesianCategories/gap/CocartesianCategoriesMethodRecord.gi +++ b/CartesianCategories/gap/CocartesianCategoriesMethodRecord.gi @@ -10,7 +10,9 @@ InstallValue( COCARTESIAN_CATEGORIES_METHOD_NAME_RECORD, rec( CocartesianCodiagonal := rec( filter_list := [ "category", "object", "integer" ], - io_type := [ [ "a", "n" ], [ "cocartesian_power", "a" ] ], + input_arguments_names := [ "cat", "a", "n" ], + output_range_getter_string := "a", + output_range_getter_preconditions := [ ], output_source_getter_string := "Coproduct( cat, ListWithIdenticalEntries( n, a ) )", output_source_getter_preconditions := [ [ "Coproduct", 1 ] ], output_range_getter_string := "a", @@ -21,7 +23,9 @@ CocartesianCodiagonal := rec( CocartesianCodiagonalWithGivenCocartesianMultiple := rec( filter_list := [ "category", "object", "integer", "object" ], - io_type := [ [ "a", "n", "cocartesian_multiple" ], [ "cocartesian_multiple", "a" ] ], + input_arguments_names := [ "cat", "a", "n", "cocartesian_multiple" ], + output_range_getter_string := "a", + output_range_getter_preconditions := [ ], output_source_getter_string := "cocartesian_multiple", output_range_getter_string := "a", return_type := "morphism", @@ -31,7 +35,7 @@ CocartesianCodiagonalWithGivenCocartesianMultiple := rec( CoproductOnMorphisms := rec( filter_list := [ "category", "morphism", "morphism" ], - io_type := [ [ "alpha", "beta" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "alpha", "beta" ], output_source_getter_string := "BinaryCoproduct( cat, Source( alpha ), Source( beta ) )", output_source_getter_preconditions := [ [ "Coproduct", 1 ] ], output_range_getter_string := "BinaryCoproduct( cat, Range( alpha ), Range( beta ) )", @@ -44,7 +48,11 @@ CoproductOnMorphisms := rec( CoproductOnMorphismsWithGivenCoproducts := rec( filter_list := [ "category", "object", "morphism", "morphism", "object" ], - io_type := [ [ "s", "alpha", "beta", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "alpha", "beta", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "DirectProductOnMorphismsWithGivenDirectProducts", dual_with_given_objects_reversed := true, @@ -52,7 +60,7 @@ CoproductOnMorphismsWithGivenCoproducts := rec( CocartesianAssociatorRightToLeft := rec( filter_list := [ "category", "object", "object", "object" ], - io_type := [ [ "a", "b", "c" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "a", "b", "c" ], output_source_getter_string := "BinaryCoproduct( cat, a, BinaryCoproduct( cat, b, c ) )", output_source_getter_preconditions := [ [ "Coproduct", 2 ] ], output_range_getter_string := "BinaryCoproduct( cat, BinaryCoproduct( cat, a, b ), c )", @@ -65,7 +73,11 @@ CocartesianAssociatorRightToLeft := rec( CocartesianAssociatorRightToLeftWithGivenCoproducts := rec( filter_list := [ "category", "object", "object", "object", "object", "object" ], - io_type := [ [ "s", "a", "b", "c", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "a", "b", "c", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "CartesianAssociatorLeftToRightWithGivenDirectProducts", dual_with_given_objects_reversed := true, @@ -73,7 +85,7 @@ CocartesianAssociatorRightToLeftWithGivenCoproducts := rec( CocartesianAssociatorLeftToRight := rec( filter_list := [ "category", "object", "object", "object" ], - io_type := [ [ "a", "b", "c" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "a", "b", "c" ], output_source_getter_string := "BinaryCoproduct( cat, BinaryCoproduct( cat, a, b ), c )", output_source_getter_preconditions := [ [ "Coproduct", 2 ] ], output_range_getter_string := "BinaryCoproduct( cat, a, BinaryCoproduct( cat, b, c ) )", @@ -86,7 +98,11 @@ CocartesianAssociatorLeftToRight := rec( CocartesianAssociatorLeftToRightWithGivenCoproducts := rec( filter_list := [ "category", "object", "object", "object", "object", "object" ], - io_type := [ [ "s", "a", "b", "c", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "a", "b", "c", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "CartesianAssociatorRightToLeftWithGivenDirectProducts", dual_with_given_objects_reversed := true, @@ -94,7 +110,9 @@ CocartesianAssociatorLeftToRightWithGivenCoproducts := rec( CocartesianLeftUnitor := rec( filter_list := [ "category", "object" ], - io_type := [ [ "a" ], [ "s", "a" ] ], + input_arguments_names := [ "cat", "a" ], + output_range_getter_string := "a", + output_range_getter_preconditions := [ ], output_source_getter_string := "BinaryCoproduct( cat, InitialObject( cat ), a )", output_source_getter_preconditions := [ [ "InitialObject", 1 ], [ "Coproduct", 1 ] ], output_range_getter_string := "a", @@ -105,7 +123,11 @@ CocartesianLeftUnitor := rec( CocartesianLeftUnitorWithGivenCoproduct := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "a", "s" ], [ "s", "a" ] ], + input_arguments_names := [ "cat", "a", "s" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "a", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "CartesianLeftUnitorInverseWithGivenDirectProduct", dual_arguments_reversed := false, @@ -113,7 +135,9 @@ CocartesianLeftUnitorWithGivenCoproduct := rec( CocartesianLeftUnitorInverse := rec( filter_list := [ "category", "object" ], - io_type := [ [ "a" ], [ "a", "r" ] ], + input_arguments_names := [ "cat", "a" ], + output_source_getter_string := "a", + output_source_getter_preconditions := [ ], output_source_getter_string := "a", output_range_getter_string := "BinaryCoproduct( cat, InitialObject( cat ), a )", output_range_getter_preconditions := [ [ "InitialObject", 1 ], [ "Coproduct", 1 ] ], @@ -124,7 +148,11 @@ CocartesianLeftUnitorInverse := rec( CocartesianLeftUnitorInverseWithGivenCoproduct := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "a", "r" ], [ "a", "r" ] ], + input_arguments_names := [ "cat", "a", "r" ], + output_source_getter_string := "a", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "CartesianLeftUnitorWithGivenDirectProduct", dual_arguments_reversed := false, @@ -132,7 +160,9 @@ CocartesianLeftUnitorInverseWithGivenCoproduct := rec( CocartesianRightUnitor := rec( filter_list := [ "category", "object" ], - io_type := [ [ "a" ], [ "s", "a" ] ], + input_arguments_names := [ "cat", "a" ], + output_range_getter_string := "a", + output_range_getter_preconditions := [ ], output_source_getter_string := "BinaryCoproduct( cat, a, InitialObject( cat ) )", output_source_getter_preconditions := [ [ "InitialObject", 1 ], [ "Coproduct", 1 ] ], output_range_getter_string := "a", @@ -143,7 +173,11 @@ CocartesianRightUnitor := rec( CocartesianRightUnitorWithGivenCoproduct := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "a", "s" ], [ "s", "a" ] ], + input_arguments_names := [ "cat", "a", "s" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "a", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "CartesianRightUnitorInverseWithGivenDirectProduct", dual_arguments_reversed := false, @@ -151,7 +185,9 @@ CocartesianRightUnitorWithGivenCoproduct := rec( CocartesianRightUnitorInverse := rec( filter_list := [ "category", "object" ], - io_type := [ [ "a" ], [ "a", "r" ] ], + input_arguments_names := [ "cat", "a" ], + output_source_getter_string := "a", + output_source_getter_preconditions := [ ], output_source_getter_string := "a", output_range_getter_string := "BinaryCoproduct( cat, a, InitialObject( cat ) )", output_range_getter_preconditions := [ [ "InitialObject", 1 ], [ "Coproduct", 1 ] ], @@ -162,7 +198,11 @@ CocartesianRightUnitorInverse := rec( CocartesianRightUnitorInverseWithGivenCoproduct := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "a", "r" ], [ "a", "r" ] ], + input_arguments_names := [ "cat", "a", "r" ], + output_source_getter_string := "a", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "CartesianRightUnitorWithGivenDirectProduct", dual_arguments_reversed := false, diff --git a/CartesianCategories/gap/CocartesianCoclosedCategoriesMethodRecord.gi b/CartesianCategories/gap/CocartesianCoclosedCategoriesMethodRecord.gi index 4f60992beb..b2736c4949 100644 --- a/CartesianCategories/gap/CocartesianCoclosedCategoriesMethodRecord.gi +++ b/CartesianCategories/gap/CocartesianCoclosedCategoriesMethodRecord.gi @@ -20,7 +20,7 @@ CoexponentialOnObjects := rec( CoexponentialOnMorphisms := rec( filter_list := [ "category", "morphism", "morphism" ], - io_type := [ [ "alpha", "beta" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "alpha", "beta" ], output_source_getter_string := "CoexponentialOnObjects( cat, Source( alpha ), Range( beta ) )", output_source_getter_preconditions := [ [ "CoexponentialOnObjects", 1 ] ], output_range_getter_string := "CoexponentialOnObjects( cat, Range( alpha ), Source( beta ) )", @@ -34,7 +34,11 @@ CoexponentialOnMorphisms := rec( CoexponentialOnMorphismsWithGivenCoexponentials := rec( filter_list := [ "category", "object", "morphism", "morphism", "object" ], - io_type := [ [ "s", "alpha", "beta", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "alpha", "beta", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "ExponentialOnMorphismsWithGivenExponentials", dual_arguments_reversed := true, @@ -42,7 +46,9 @@ CoexponentialOnMorphismsWithGivenCoexponentials := rec( CocartesianEvaluationMorphism := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "a", "b" ], [ "a", "r" ] ], + input_arguments_names := [ "cat", "a", "b" ], + output_source_getter_string := "a", + output_source_getter_preconditions := [ ], output_source_getter_string := "a", output_range_getter_string := "BinaryCoproduct( cat, CoexponentialOnObjects( cat, a, b ), b )", output_range_getter_preconditions := [ [ "Coproduct", 1 ], [ "CoexponentialOnObjects", 1 ] ], @@ -55,7 +61,11 @@ CocartesianEvaluationMorphism := rec( CocartesianEvaluationMorphismWithGivenRange := rec( filter_list := [ "category", "object", "object", "object" ], - io_type := [ [ "a", "b", "r" ], [ "a", "r" ] ], + input_arguments_names := [ "cat", "a", "b", "r" ], + output_source_getter_string := "a", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "CartesianEvaluationMorphismWithGivenSource", dual_preprocessor_func := { cat, a, b, r } -> NTuple( 4, Opposite( cat ), Opposite( b ), Opposite( a ), Opposite( r ) ), @@ -64,7 +74,9 @@ CocartesianEvaluationMorphismWithGivenRange := rec( CocartesianCoevaluationMorphism := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "a", "b" ], [ "s", "a" ] ], + input_arguments_names := [ "cat", "a", "b" ], + output_range_getter_string := "a", + output_range_getter_preconditions := [ ], output_source_getter_string := "CoexponentialOnObjects( cat, BinaryCoproduct( cat, a, b ), b )", output_source_getter_preconditions := [ [ "CoexponentialOnObjects", 1 ], [ "Coproduct", 1 ] ], output_range_getter_string := "a", @@ -77,7 +89,11 @@ CocartesianCoevaluationMorphism := rec( CocartesianCoevaluationMorphismWithGivenSource := rec( filter_list := [ "category", "object", "object", "object" ], - io_type := [ [ "a", "b", "s" ], [ "s", "a" ] ], + input_arguments_names := [ "cat", "a", "b", "s" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "a", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "CartesianCoevaluationMorphismWithGivenRange", dual_arguments_reversed := false, @@ -85,7 +101,9 @@ CocartesianCoevaluationMorphismWithGivenSource := rec( CoproductToCoexponentialAdjunctionMap := rec( filter_list := [ "category", "object", "object", "morphism" ], - io_type := [ [ "c", "b", "g" ], [ "i", "c" ] ], + input_arguments_names := [ "cat", "c", "b", "g" ], + output_range_getter_string := "c", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "DirectProductToExponentialAdjunctionMap", dual_arguments_reversed := false, @@ -94,7 +112,11 @@ CoproductToCoexponentialAdjunctionMap := rec( CoproductToCoexponentialAdjunctionMapWithGivenCoexponential := rec( filter_list := [ "category", "object", "object", "morphism", "object" ], - io_type := [ [ "c", "b", "g", "i" ], [ "i", "c" ] ], + input_arguments_names := [ "cat", "c", "b", "g", "i" ], + output_source_getter_string := "i", + output_source_getter_preconditions := [ ], + output_range_getter_string := "c", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "DirectProductToExponentialAdjunctionMapWithGivenExponential", dual_arguments_reversed := false, @@ -102,7 +124,9 @@ CoproductToCoexponentialAdjunctionMapWithGivenCoexponential := rec( CoexponentialToCoproductAdjunctionMap := rec( filter_list := [ "category", "object", "object", "morphism" ], - io_type := [ [ "a", "b", "f", ], [ "a", "t" ] ], + input_arguments_names := [ "cat", "a", "b", "f" ], + output_source_getter_string := "a", + output_source_getter_preconditions := [ ], return_type := "morphism", dual_operation := "ExponentialToDirectProductAdjunctionMap", dual_preprocessor_func := { cat, a, b, f } -> NTuple( 4, Opposite( cat ), Opposite( b ), Opposite( a ), Opposite( f ) ), @@ -112,7 +136,11 @@ CoexponentialToCoproductAdjunctionMap := rec( CoexponentialToCoproductAdjunctionMapWithGivenCoproduct := rec( filter_list := [ "category", "object", "object", "morphism", "object" ], - io_type := [ [ "a", "b", "f", "t" ], [ "a", "t" ] ], + input_arguments_names := [ "cat", "a", "b", "f", "t" ], + output_source_getter_string := "a", + output_source_getter_preconditions := [ ], + output_range_getter_string := "t", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "ExponentialToDirectProductAdjunctionMapWithGivenDirectProduct", dual_preprocessor_func := { cat, a, b, f, t } -> NTuple( 4, Opposite( cat ), Opposite( b ), Opposite( a ), Opposite( f ), Opposite( t ) ), @@ -121,7 +149,7 @@ CoexponentialToCoproductAdjunctionMapWithGivenCoproduct := rec( CocartesianPreCoComposeMorphism := rec( filter_list := [ "category", "object", "object", "object" ], - io_type := [ [ "a", "b", "c" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "a", "b", "c" ], output_source_getter_string := "CoexponentialOnObjects( cat, a, c )", output_source_getter_preconditions := [ [ "CoexponentialOnObjects", 1 ] ], output_range_getter_string := "BinaryCoproduct( cat, CoexponentialOnObjects( cat, b, c ), CoexponentialOnObjects( cat, a, b ) )", @@ -135,7 +163,11 @@ CocartesianPreCoComposeMorphism := rec( CocartesianPreCoComposeMorphismWithGivenObjects := rec( filter_list := [ "category", "object", "object", "object", "object", "object" ], - io_type := [ [ "s", "a", "b", "c", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "a", "b", "c", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "CartesianPreComposeMorphismWithGivenObjects", dual_arguments_reversed := true, @@ -143,7 +175,7 @@ CocartesianPreCoComposeMorphismWithGivenObjects := rec( CocartesianPostCoComposeMorphism := rec( filter_list := [ "category", "object", "object", "object" ], - io_type := [ [ "a", "b", "c" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "a", "b", "c" ], output_source_getter_string := "CoexponentialOnObjects( cat, a, c )", output_source_getter_preconditions := [ [ "CoexponentialOnObjects", 1 ] ], output_range_getter_string := "BinaryCoproduct( cat, CoexponentialOnObjects( cat, a, b ), CoexponentialOnObjects( cat, b, c ) )", @@ -157,7 +189,11 @@ CocartesianPostCoComposeMorphism := rec( CocartesianPostCoComposeMorphismWithGivenObjects := rec( filter_list := [ "category", "object", "object", "object", "object", "object" ], - io_type := [ [ "s", "a", "b", "c", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "a", "b", "c", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "CartesianPostComposeMorphismWithGivenObjects", dual_arguments_reversed := true, @@ -173,7 +209,7 @@ CocartesianDualOnObjects := rec( CocartesianDualOnMorphisms := rec( filter_list := [ "category", "morphism" ], - io_type := [ [ "alpha" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "alpha" ], output_source_getter_string := "CocartesianDualOnObjects( cat, Range( alpha ) )", output_source_getter_preconditions := [ [ "CocartesianDualOnObjects", 1 ] ], output_range_getter_string := "CocartesianDualOnObjects( cat, Source( alpha ) )", @@ -186,7 +222,11 @@ CocartesianDualOnMorphisms := rec( CocartesianDualOnMorphismsWithGivenCocartesianDuals := rec( filter_list := [ "category", "object", "morphism", "object" ], - io_type := [ [ "s", "alpha", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "alpha", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "CartesianDualOnMorphismsWithGivenCartesianDuals", dual_arguments_reversed := true, @@ -194,7 +234,7 @@ CocartesianDualOnMorphismsWithGivenCocartesianDuals := rec( CocartesianEvaluationForCocartesianDual := rec( filter_list := [ "category", "object" ], - io_type := [ [ "a" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "a" ], output_source_getter_string := "InitialObject( cat )", output_source_getter_preconditions := [ [ "InitialObject", 1 ] ], output_range_getter_string := "BinaryCoproduct( cat, CocartesianDualOnObjects( cat, a ), a )", @@ -207,7 +247,11 @@ CocartesianEvaluationForCocartesianDual := rec( CocartesianEvaluationForCocartesianDualWithGivenCoproduct := rec( filter_list := [ "category", "object", "object", "object" ], - io_type := [ [ "s", "a", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "a", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "CartesianEvaluationForCartesianDualWithGivenDirectProduct", dual_arguments_reversed := true, @@ -215,7 +259,9 @@ CocartesianEvaluationForCocartesianDualWithGivenCoproduct := rec( MorphismFromCocartesianBidual := rec( filter_list := [ "category", "object" ], - io_type := [ [ "a" ], [ "s", "a" ] ], + input_arguments_names := [ "cat", "a" ], + output_range_getter_string := "a", + output_range_getter_preconditions := [ ], output_source_getter_string := "CocartesianDualOnObjects( cat, CocartesianDualOnObjects( cat, a ) )", output_source_getter_preconditions := [ [ "CocartesianDualOnObjects", 2 ] ], output_range_getter_string := "a", @@ -227,7 +273,11 @@ MorphismFromCocartesianBidual := rec( MorphismFromCocartesianBidualWithGivenCocartesianBidual := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "a", "s" ], [ "s", "a" ] ], + input_arguments_names := [ "cat", "a", "s" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "a", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "MorphismToCartesianBidualWithGivenCartesianBidual", dual_arguments_reversed := false, @@ -262,7 +312,7 @@ CoexponentialCoproductCompatibilityMorphismWithGivenObjects := rec( CocartesianDualityCoproductCompatibilityMorphism := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "a", "b" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "a", "b" ], output_source_getter_string := "CocartesianDualOnObjects( cat, BinaryCoproduct( cat, a, b ) )", output_source_getter_preconditions := [ [ "CocartesianDualOnObjects", 1 ], [ "Coproduct", 1 ] ], output_range_getter_string := "BinaryCoproduct( cat, CocartesianDualOnObjects( cat, a ), CocartesianDualOnObjects( cat, b ) )", @@ -276,7 +326,11 @@ CocartesianDualityCoproductCompatibilityMorphism := rec( CocartesianDualityCoproductCompatibilityMorphismWithGivenObjects := rec( filter_list := [ "category", "object", "object", "object", "object" ], - io_type := [ [ "s", "a", "b", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "a", "b", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "DirectProductCartesianDualityCompatibilityMorphismWithGivenObjects", dual_with_given_objects_reversed := true, @@ -284,7 +338,7 @@ CocartesianDualityCoproductCompatibilityMorphismWithGivenObjects := rec( MorphismFromCoexponentialToCoproduct := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "a", "b" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "a", "b" ], output_source_getter_string := "CoexponentialOnObjects( cat, a, b )", output_source_getter_preconditions := [ [ "CoexponentialOnObjects", 1 ] ], output_range_getter_string := "BinaryCoproduct( cat, CocartesianDualOnObjects( cat, b ), a )", @@ -298,7 +352,11 @@ MorphismFromCoexponentialToCoproduct := rec( MorphismFromCoexponentialToCoproductWithGivenObjects := rec( filter_list := [ "category", "object", "object", "object", "object" ], - io_type := [ [ "s", "a", "b", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "a", "b", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "MorphismFromDirectProductToExponentialWithGivenObjects", dual_arguments_reversed := true, @@ -306,7 +364,7 @@ MorphismFromCoexponentialToCoproductWithGivenObjects := rec( IsomorphismFromCocartesianDualObjectToCoexponentialFromInitialObject := rec( filter_list := [ "category", "object" ], - io_type := [ [ "a" ], [ "d", "i" ] ], + input_arguments_names := [ "cat", "a" ], output_source_getter_string := "CocartesianDualOnObjects( cat, a )", output_source_getter_preconditions := [ [ "CocartesianDualOnObjects", 1 ] ], output_range_getter_string := "CoexponentialOnObjects( cat, InitialObject( cat ), a )", @@ -318,7 +376,7 @@ IsomorphismFromCocartesianDualObjectToCoexponentialFromInitialObject := rec( IsomorphismFromCoexponentialFromInitialObjectToCocartesianDualObject := rec( filter_list := [ "category", "object" ], - io_type := [ [ "a" ], [ "i", "d" ] ], + input_arguments_names := [ "cat", "a" ], output_source_getter_string := "CoexponentialOnObjects( cat, InitialObject( cat ), a )", output_source_getter_preconditions := [ [ "CoexponentialOnObjects", 1 ], [ "InitialObject", 1 ] ], output_range_getter_string := "CocartesianDualOnObjects( cat, a )", @@ -330,7 +388,9 @@ IsomorphismFromCoexponentialFromInitialObjectToCocartesianDualObject := rec( UniversalPropertyOfCocartesianDual := rec( filter_list := [ "category", "object", "object", "morphism" ], - io_type := [ [ "t", "a", "alpha" ], [ "d", "t" ] ], + input_arguments_names := [ "cat", "t", "a", "alpha" ], + output_range_getter_string := "t", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "UniversalPropertyOfCartesianDual", dual_arguments_reversed := false, @@ -339,7 +399,7 @@ UniversalPropertyOfCocartesianDual := rec( CocartesianLambdaIntroduction := rec( filter_list := [ "category", "morphism" ], - io_type := [ [ "alpha" ], [ "u", "i" ] ], + input_arguments_names := [ "cat", "alpha" ], return_type := "morphism", dual_operation := "CartesianLambdaIntroduction", # Test in CocartesianCoclosedCategoriesTest @@ -347,7 +407,11 @@ CocartesianLambdaIntroduction := rec( CocartesianLambdaElimination := rec( filter_list := [ "category", "object", "object", "morphism" ], - io_type := [ [ "a", "b", "alpha" ], [ "a", "b" ] ], + input_arguments_names := [ "cat", "a", "b", "alpha" ], + output_source_getter_string := "a", + output_source_getter_preconditions := [ ], + output_range_getter_string := "b", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "CartesianLambdaElimination", dual_preprocessor_func := { cat, a, b, alpha } -> NTuple( 4, Opposite( cat ), Opposite( b ), Opposite( a ), Opposite( alpha ) ), @@ -357,7 +421,9 @@ CocartesianLambdaElimination := rec( IsomorphismFromObjectToCoexponential := rec( filter_list := [ "category", "object" ], - io_type := [ [ "a" ], [ "a", "r" ] ], + input_arguments_names := [ "cat", "a" ], + output_source_getter_string := "a", + output_source_getter_preconditions := [ ], output_source_getter_string := "a", output_range_getter_string := "CoexponentialOnObjects( cat, a, InitialObject( cat ) )", output_range_getter_preconditions := [ [ "CoexponentialOnObjects", 1 ], [ "InitialObject", 1 ] ], @@ -369,7 +435,11 @@ IsomorphismFromObjectToCoexponential := rec( IsomorphismFromObjectToCoexponentialWithGivenCoexponential := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "a", "r" ], [ "a", "r" ] ], + input_arguments_names := [ "cat", "a", "r" ], + output_source_getter_string := "a", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "IsomorphismFromExponentialToObjectWithGivenExponential", dual_arguments_reversed := false, @@ -377,7 +447,9 @@ IsomorphismFromObjectToCoexponentialWithGivenCoexponential := rec( IsomorphismFromCoexponentialToObject := rec( filter_list := [ "category", "object" ], - io_type := [ [ "a" ], [ "s", "a" ] ], + input_arguments_names := [ "cat", "a" ], + output_range_getter_string := "a", + output_range_getter_preconditions := [ ], output_source_getter_string := "CoexponentialOnObjects( cat, a, InitialObject( cat ) )", output_source_getter_preconditions := [ [ "CoexponentialOnObjects", 1 ], [ "InitialObject", 1 ] ], output_range_getter_string := "a", @@ -389,7 +461,11 @@ IsomorphismFromCoexponentialToObject := rec( IsomorphismFromCoexponentialToObjectWithGivenCoexponential := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "a", "s" ], [ "s", "a" ] ], + input_arguments_names := [ "cat", "a", "s" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "a", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "IsomorphismFromObjectToExponentialWithGivenExponential", dual_arguments_reversed := false, diff --git a/CartesianCategories/gap/CodistributiveCocartesianCategoriesMethodRecord.gi b/CartesianCategories/gap/CodistributiveCocartesianCategoriesMethodRecord.gi index 5badf255cf..818c20c15a 100644 --- a/CartesianCategories/gap/CodistributiveCocartesianCategoriesMethodRecord.gi +++ b/CartesianCategories/gap/CodistributiveCocartesianCategoriesMethodRecord.gi @@ -11,7 +11,7 @@ InstallValue( CODISTRIBUTIVE_COCARTESIAN_CATEGORIES_METHOD_NAME_RECORD, rec( LeftCocartesianCodistributivityExpanding := rec( filter_list := [ "category", "object", "list_of_objects" ], - io_type := [ [ "a", "L" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "a", "L" ], output_source_getter_string := "BinaryCoproduct( cat, a, DirectProduct( cat, L ) )", output_source_getter_preconditions := [ [ "DirectProduct", 1 ], [ "Coproduct", 1 ] ], output_range_getter_string := "DirectProduct( cat, List( L, summand -> BinaryCoproduct( cat, a, summand ) ) )", @@ -25,7 +25,11 @@ LeftCocartesianCodistributivityExpanding := rec( LeftCocartesianCodistributivityExpandingWithGivenObjects := rec( filter_list := [ "category", "object", "object", "list_of_objects", "object" ], - io_type := [ [ "s", "a", "L", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "a", "L", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "LeftCartesianDistributivityFactoringWithGivenObjects", dual_with_given_objects_reversed := true, @@ -34,7 +38,7 @@ LeftCocartesianCodistributivityExpandingWithGivenObjects := rec( LeftCocartesianCodistributivityFactoring := rec( filter_list := [ "category", "object", "list_of_objects" ], - io_type := [ [ "a", "L" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "a", "L" ], output_source_getter_string := "DirectProduct( cat, List( L, summand -> BinaryCoproduct( cat, a, summand ) ) )", output_source_getter_preconditions := [ [ "DirectProduct", 1 ], [ "Coproduct", 2 ] ], output_range_getter_string := "BinaryCoproduct( cat, a, DirectProduct( cat, L ) )", @@ -48,7 +52,11 @@ LeftCocartesianCodistributivityFactoring := rec( LeftCocartesianCodistributivityFactoringWithGivenObjects := rec( filter_list := [ "category", "object", "object", "list_of_objects", "object" ], - io_type := [ [ "s", "a", "L", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "a", "L", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "LeftCartesianDistributivityExpandingWithGivenObjects", dual_with_given_objects_reversed := true, @@ -57,7 +65,7 @@ LeftCocartesianCodistributivityFactoringWithGivenObjects := rec( RightCocartesianCodistributivityExpanding := rec( filter_list := [ "category", "list_of_objects", "object" ], - io_type := [ [ "L", "a" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "L", "a" ], output_source_getter_string := "BinaryCoproduct( cat, DirectProduct( cat, L ), a )", output_source_getter_preconditions := [ [ "DirectProduct", 1 ], [ "Coproduct", 1 ] ], output_range_getter_string := "DirectProduct( cat, List( L, summand -> BinaryCoproduct( cat, summand, a ) ) )", @@ -71,7 +79,11 @@ RightCocartesianCodistributivityExpanding := rec( RightCocartesianCodistributivityExpandingWithGivenObjects := rec( filter_list := [ "category", "object", "list_of_objects", "object", "object" ], - io_type := [ [ "s", "L", "a", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "L", "a", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "RightCartesianDistributivityFactoringWithGivenObjects", dual_with_given_objects_reversed := true, @@ -80,7 +92,7 @@ RightCocartesianCodistributivityExpandingWithGivenObjects := rec( RightCocartesianCodistributivityFactoring := rec( filter_list := [ "category", "list_of_objects", "object" ], - io_type := [ [ "L", "a" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "L", "a" ], output_source_getter_string := "DirectProduct( cat, List( L, summand -> BinaryCoproduct( cat, summand, a ) ) )", output_source_getter_preconditions := [ [ "DirectProduct", 1 ], [ "Coproduct", 2 ] ], output_range_getter_string := "BinaryCoproduct( cat, DirectProduct( cat, L ), a )", @@ -94,7 +106,11 @@ RightCocartesianCodistributivityFactoring := rec( RightCocartesianCodistributivityFactoringWithGivenObjects := rec( filter_list := [ "category", "object", "list_of_objects", "object", "object" ], - io_type := [ [ "s", "L", "a", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "L", "a", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "RightCartesianDistributivityExpandingWithGivenObjects", dual_with_given_objects_reversed := true, diff --git a/CartesianCategories/gap/DistributiveCartesianCategoriesMethodRecord.gi b/CartesianCategories/gap/DistributiveCartesianCategoriesMethodRecord.gi index 3bb03d5376..7e4cbea51c 100644 --- a/CartesianCategories/gap/DistributiveCartesianCategoriesMethodRecord.gi +++ b/CartesianCategories/gap/DistributiveCartesianCategoriesMethodRecord.gi @@ -11,7 +11,7 @@ InstallValue( DISTRIBUTIVE_CARTESIAN_CATEGORIES_METHOD_NAME_RECORD, rec( LeftCartesianDistributivityExpanding := rec( filter_list := [ "category", "object", "list_of_objects" ], - io_type := [ [ "a", "L" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "a", "L" ], output_source_getter_string := "BinaryDirectProduct( cat, a, Coproduct( cat, L ) )", output_source_getter_preconditions := [ [ "Coproduct", 1 ], [ "DirectProduct", 1 ] ], output_range_getter_string := "Coproduct( cat, List( L, summand -> BinaryDirectProduct( cat, a, summand ) ) )", @@ -25,7 +25,11 @@ LeftCartesianDistributivityExpanding := rec( LeftCartesianDistributivityExpandingWithGivenObjects := rec( filter_list := [ "category", "object", "object", "list_of_objects", "object" ], - io_type := [ [ "s", "a", "L", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "a", "L", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "LeftCocartesianCodistributivityFactoringWithGivenObjects", dual_with_given_objects_reversed := true, @@ -34,7 +38,7 @@ LeftCartesianDistributivityExpandingWithGivenObjects := rec( LeftCartesianDistributivityFactoring := rec( filter_list := [ "category", "object", "list_of_objects" ], - io_type := [ [ "a", "L" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "a", "L" ], output_source_getter_string := "Coproduct( cat, List( L, summand -> BinaryDirectProduct( cat, a, summand ) ) )", output_source_getter_preconditions := [ [ "Coproduct", 1 ], [ "DirectProduct", 2 ] ], output_range_getter_string := "BinaryDirectProduct( cat, a, Coproduct( cat, L ) )", @@ -48,7 +52,11 @@ LeftCartesianDistributivityFactoring := rec( LeftCartesianDistributivityFactoringWithGivenObjects := rec( filter_list := [ "category", "object", "object", "list_of_objects", "object" ], - io_type := [ [ "s", "a", "L", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "a", "L", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "LeftCocartesianCodistributivityExpandingWithGivenObjects", dual_with_given_objects_reversed := true, @@ -57,7 +65,7 @@ LeftCartesianDistributivityFactoringWithGivenObjects := rec( RightCartesianDistributivityExpanding := rec( filter_list := [ "category", "list_of_objects", "object" ], - io_type := [ [ "L", "a" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "L", "a" ], output_source_getter_string := "BinaryDirectProduct( cat, Coproduct( cat, L ), a )", output_source_getter_preconditions := [ [ "Coproduct", 1 ], [ "DirectProduct", 1 ] ], output_range_getter_string := "Coproduct( cat, List( L, summand -> BinaryDirectProduct( cat, summand, a ) ) )", @@ -71,7 +79,11 @@ RightCartesianDistributivityExpanding := rec( RightCartesianDistributivityExpandingWithGivenObjects := rec( filter_list := [ "category", "object", "list_of_objects", "object", "object" ], - io_type := [ [ "s", "L", "a", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "L", "a", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "RightCocartesianCodistributivityFactoringWithGivenObjects", dual_with_given_objects_reversed := true, @@ -80,7 +92,7 @@ RightCartesianDistributivityExpandingWithGivenObjects := rec( RightCartesianDistributivityFactoring := rec( filter_list := [ "category", "list_of_objects", "object" ], - io_type := [ [ "L", "a" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "L", "a" ], output_source_getter_string := "Coproduct( cat, List( L, summand -> BinaryDirectProduct( cat, summand, a ) ) )", output_source_getter_preconditions := [ [ "Coproduct", 1 ], [ "DirectProduct", 2 ] ], output_range_getter_string := "BinaryDirectProduct( cat, Coproduct( cat, L ), a )", @@ -94,7 +106,11 @@ RightCartesianDistributivityFactoring := rec( RightCartesianDistributivityFactoringWithGivenObjects := rec( filter_list := [ "category", "object", "list_of_objects", "object", "object" ], - io_type := [ [ "s", "L", "a", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "L", "a", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "RightCocartesianCodistributivityExpandingWithGivenObjects", dual_with_given_objects_reversed := true, diff --git a/FreydCategoriesForCAP/PackageInfo.g b/FreydCategoriesForCAP/PackageInfo.g index e03f21e5ae..6c516d9a53 100644 --- a/FreydCategoriesForCAP/PackageInfo.g +++ b/FreydCategoriesForCAP/PackageInfo.g @@ -10,7 +10,7 @@ SetPackageInfo( rec( PackageName := "FreydCategoriesForCAP", Subtitle := "Freyd categories - Formal (co)kernels for additive categories", -Version := "2023.07-01", +Version := "2023.07-02", 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/FreydCategoriesForCAP/gap/FreydCategoriesForCAP.gi b/FreydCategoriesForCAP/gap/FreydCategoriesForCAP.gi index 355d211fa8..7ca94df112 100644 --- a/FreydCategoriesForCAP/gap/FreydCategoriesForCAP.gi +++ b/FreydCategoriesForCAP/gap/FreydCategoriesForCAP.gi @@ -113,7 +113,9 @@ WeakKernelObject := rec( WeakKernelEmbedding := rec( filter_list := [ "category", "morphism" ], - io_type := [ [ "alpha" ], [ "K", "alpha_source" ] ], + input_arguments_names := [ "cat", "alpha" ], + output_range_getter_string := "Source( alpha )", + output_range_getter_preconditions := [ ], with_given_object_position := "Source", return_type := "morphism", dual_operation := "WeakCokernelProjection", @@ -121,14 +123,20 @@ WeakKernelEmbedding := rec( WeakKernelEmbeddingWithGivenWeakKernelObject := rec( filter_list := [ "category", "morphism", "object" ], - io_type := [ [ "alpha", "K" ], [ "K", "alpha_source" ] ], + input_arguments_names := [ "cat", "alpha", "K" ], + output_source_getter_string := "K", + output_source_getter_preconditions := [ ], + output_range_getter_string := "Source( alpha )", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "WeakCokernelProjectionWithGivenWeakCokernelObject", is_merely_set_theoretic := true ), WeakKernelLift := rec( filter_list := [ "category", "morphism", "morphism" ], - io_type := [ [ "alpha", "tau" ], [ "tau_source", "K" ] ], + input_arguments_names := [ "cat", "alpha", "tau" ], + output_source_getter_string := "Source( tau )", + output_source_getter_preconditions := [ ], with_given_object_position := "Range", return_type := "morphism", dual_operation := "WeakCokernelColift", @@ -136,7 +144,11 @@ WeakKernelLift := rec( WeakKernelLiftWithGivenWeakKernelObject := rec( filter_list := [ "category", "morphism", "morphism", "object" ], - io_type := [ [ "alpha", "tau", "K" ], [ "tau_source", "K" ] ], + input_arguments_names := [ "cat", "alpha", "tau", "K" ], + output_source_getter_string := "Source( tau )", + output_source_getter_preconditions := [ ], + output_range_getter_string := "K", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "WeakCokernelColiftWithGivenWeakCokernelObject", is_merely_set_theoretic := true ), @@ -151,7 +163,9 @@ WeakCokernelObject := rec( WeakCokernelProjection := rec( filter_list := [ "category", "morphism" ], - io_type := [ [ "alpha" ], [ "alpha_range", "K" ] ], + input_arguments_names := [ "cat", "alpha" ], + output_source_getter_string := "Range( alpha )", + output_source_getter_preconditions := [ ], with_given_object_position := "Range", return_type := "morphism", dual_operation := "WeakKernelEmbedding", @@ -159,14 +173,20 @@ WeakCokernelProjection := rec( WeakCokernelProjectionWithGivenWeakCokernelObject := rec( filter_list := [ "category", "morphism", "object" ], - io_type := [ [ "alpha", "K" ], [ "alpha_range", "K" ] ], + input_arguments_names := [ "cat", "alpha", "K" ], + output_source_getter_string := "Range( alpha )", + output_source_getter_preconditions := [ ], + output_range_getter_string := "K", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "WeakKernelEmbeddingWithGivenWeakKernelObject", is_merely_set_theoretic := true ), WeakCokernelColift := rec( filter_list := [ "category", "morphism", "morphism" ], - io_type := [ [ "alpha", "tau" ], [ "K", "tau_range" ] ], + input_arguments_names := [ "cat", "alpha", "tau" ], + output_range_getter_string := "Range( tau )", + output_range_getter_preconditions := [ ], with_given_object_position := "Source", return_type := "morphism", dual_operation := "WeakKernelLift", @@ -174,7 +194,11 @@ WeakCokernelColift := rec( WeakCokernelColiftWithGivenWeakCokernelObject := rec( filter_list := [ "category", "morphism", "morphism", "object" ], - io_type := [ [ "alpha", "tau", "K" ], [ "K", "tau_range" ] ], + input_arguments_names := [ "cat", "alpha", "tau", "K" ], + output_source_getter_string := "K", + output_source_getter_preconditions := [ ], + output_range_getter_string := "Range( tau )", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "WeakKernelLiftWithGivenWeakKernelObject", is_merely_set_theoretic := true ), @@ -190,7 +214,9 @@ WeakBiFiberProduct := rec( ProjectionInFirstFactorOfWeakBiFiberProduct := rec( filter_list := [ "category", "morphism", "morphism" ], - io_type := [ [ "a", "b" ], [ "P", "a_source" ] ], + input_arguments_names := [ "cat", "a", "b" ], + output_range_getter_string := "Source( a )", + output_range_getter_preconditions := [ ], with_given_object_position := "Source", dual_operation := "InjectionOfFirstCofactorOfWeakBiPushout", pre_function := WEAK_BI_FIBER_PRODUCT_PREFUNCTION, @@ -199,7 +225,11 @@ ProjectionInFirstFactorOfWeakBiFiberProduct := rec( ProjectionInFirstFactorOfWeakBiFiberProductWithGivenWeakBiFiberProduct := rec( filter_list := [ "category", "morphism", "morphism", "object" ], - io_type := [ [ "a", "b", "P" ], [ "P", "a_source" ] ], + input_arguments_names := [ "cat", "a", "b", "P" ], + output_source_getter_string := "P", + output_source_getter_preconditions := [ ], + output_range_getter_string := "Source( a )", + output_range_getter_preconditions := [ ], dual_operation := "InjectionOfFirstCofactorOfWeakBiPushoutWithGivenWeakBiPushout", pre_function := WEAK_BI_FIBER_PRODUCT_PREFUNCTION, return_type := "morphism", @@ -207,7 +237,9 @@ ProjectionInFirstFactorOfWeakBiFiberProductWithGivenWeakBiFiberProduct := rec( ProjectionInSecondFactorOfWeakBiFiberProduct := rec( filter_list := [ "category", "morphism", "morphism" ], - io_type := [ [ "a", "b" ], [ "P", "b_source" ] ], + input_arguments_names := [ "cat", "a", "b" ], + output_range_getter_string := "Source( b )", + output_range_getter_preconditions := [ ], with_given_object_position := "Source", dual_operation := "InjectionOfSecondCofactorOfWeakBiPushout", pre_function := WEAK_BI_FIBER_PRODUCT_PREFUNCTION, @@ -216,7 +248,11 @@ ProjectionInSecondFactorOfWeakBiFiberProduct := rec( ProjectionInSecondFactorOfWeakBiFiberProductWithGivenWeakBiFiberProduct := rec( filter_list := [ "category", "morphism", "morphism", "object" ], - io_type := [ [ "a", "b", "P" ], [ "P", "b_source" ] ], + input_arguments_names := [ "cat", "a", "b", "P" ], + output_source_getter_string := "P", + output_source_getter_preconditions := [ ], + output_range_getter_string := "Source( b )", + output_range_getter_preconditions := [ ], dual_operation := "InjectionOfSecondCofactorOfWeakBiPushoutWithGivenWeakBiPushout", pre_function := WEAK_BI_FIBER_PRODUCT_PREFUNCTION, return_type := "morphism", @@ -224,7 +260,9 @@ ProjectionInSecondFactorOfWeakBiFiberProductWithGivenWeakBiFiberProduct := rec( UniversalMorphismIntoWeakBiFiberProduct := rec( filter_list := [ "category", "morphism", "morphism", "morphism", "morphism" ], - io_type := [ [ "a", "b", "t", "s" ], [ "t_source", "P" ] ], + input_arguments_names := [ "cat", "a", "b", "t", "s" ], + output_source_getter_string := "Source( t )", + output_source_getter_preconditions := [ ], with_given_object_position := "Range", dual_operation := "UniversalMorphismFromWeakBiPushout", pre_function := UNIVERSAL_MORPHISM_INTO_WEAK_BI_FIBER_PRODUCT_PREFUNCTION, @@ -233,7 +271,11 @@ UniversalMorphismIntoWeakBiFiberProduct := rec( UniversalMorphismIntoWeakBiFiberProductWithGivenWeakBiFiberProduct := rec( filter_list := [ "category", "morphism", "morphism", "morphism", "morphism", "object" ], - io_type := [ [ "a", "b", "t", "s", "P", ], [ "t_source", "P" ] ], + input_arguments_names := [ "cat", "a", "b", "t", "s", "P" ], + output_source_getter_string := "Source( t )", + output_source_getter_preconditions := [ ], + output_range_getter_string := "P", + output_range_getter_preconditions := [ ], dual_operation := "UniversalMorphismFromWeakBiPushoutWithGivenWeakBiPushout", pre_function := UNIVERSAL_MORPHISM_INTO_WEAK_BI_FIBER_PRODUCT_PREFUNCTION, return_type := "morphism", @@ -241,7 +283,7 @@ UniversalMorphismIntoWeakBiFiberProductWithGivenWeakBiFiberProduct := rec( WeakBiFiberProductMorphismToDirectSum := rec( filter_list := [ "category", "morphism", "morphism" ], - io_type := [ [ "alpha", "beta" ], [ "F", "S" ] ], + input_arguments_names := [ "cat", "alpha", "beta" ], return_type := "morphism", dual_operation := "DirectSumMorphismToWeakBiPushout", ), @@ -257,7 +299,9 @@ WeakBiPushout := rec( InjectionOfFirstCofactorOfWeakBiPushout := rec( filter_list := [ "category", "morphism", "morphism" ], - io_type := [ [ "a", "b" ], [ "a_range", "P" ] ], + input_arguments_names := [ "cat", "a", "b" ], + output_source_getter_string := "Range( a )", + output_source_getter_preconditions := [ ], with_given_object_position := "Range", dual_operation := "ProjectionInFirstFactorOfWeakBiFiberProduct", pre_function := WEAK_BI_PUSHOUT_PREFUNCTION, @@ -266,7 +310,11 @@ InjectionOfFirstCofactorOfWeakBiPushout := rec( InjectionOfFirstCofactorOfWeakBiPushoutWithGivenWeakBiPushout := rec( filter_list := [ "category", "morphism", "morphism", "object" ], - io_type := [ [ "a", "b", "P" ], [ "a_range", "P" ] ], + input_arguments_names := [ "cat", "a", "b", "P" ], + output_source_getter_string := "Range( a )", + output_source_getter_preconditions := [ ], + output_range_getter_string := "P", + output_range_getter_preconditions := [ ], dual_operation := "ProjectionInFirstFactorOfWeakBiFiberProductWithGivenWeakBiFiberProduct", pre_function := WEAK_BI_PUSHOUT_PREFUNCTION, return_type := "morphism", @@ -274,7 +322,9 @@ InjectionOfFirstCofactorOfWeakBiPushoutWithGivenWeakBiPushout := rec( InjectionOfSecondCofactorOfWeakBiPushout := rec( filter_list := [ "category", "morphism", "morphism" ], - io_type := [ [ "a", "b" ], [ "b_range", "P" ] ], + input_arguments_names := [ "cat", "a", "b" ], + output_source_getter_string := "Range( b )", + output_source_getter_preconditions := [ ], with_given_object_position := "Range", dual_operation := "ProjectionInSecondFactorOfWeakBiFiberProduct", pre_function := WEAK_BI_PUSHOUT_PREFUNCTION, @@ -283,7 +333,11 @@ InjectionOfSecondCofactorOfWeakBiPushout := rec( InjectionOfSecondCofactorOfWeakBiPushoutWithGivenWeakBiPushout := rec( filter_list := [ "category", "morphism", "morphism", "object" ], - io_type := [ [ "a", "b", "P" ], [ "b_range", "P" ] ], + input_arguments_names := [ "cat", "a", "b", "P" ], + output_source_getter_string := "Range( b )", + output_source_getter_preconditions := [ ], + output_range_getter_string := "P", + output_range_getter_preconditions := [ ], dual_operation := "ProjectionInSecondFactorOfWeakBiFiberProductWithGivenWeakBiFiberProduct", pre_function := WEAK_BI_PUSHOUT_PREFUNCTION, return_type := "morphism", @@ -291,7 +345,9 @@ InjectionOfSecondCofactorOfWeakBiPushoutWithGivenWeakBiPushout := rec( UniversalMorphismFromWeakBiPushout := rec( filter_list := [ "category", "morphism", "morphism", "morphism", "morphism" ], - io_type := [ [ "a", "b", "t", "s" ], [ "P", "t_range" ] ], + input_arguments_names := [ "cat", "a", "b", "t", "s" ], + output_range_getter_string := "Range( t )", + output_range_getter_preconditions := [ ], with_given_object_position := "Source", dual_operation := "UniversalMorphismIntoWeakBiFiberProduct", pre_function := UNIVERSAL_MORPHISM_FROM_WEAK_BI_PUSHOUT_PREFUNCTION, @@ -300,7 +356,11 @@ UniversalMorphismFromWeakBiPushout := rec( UniversalMorphismFromWeakBiPushoutWithGivenWeakBiPushout := rec( filter_list := [ "category", "morphism", "morphism", "morphism", "morphism", "object" ], - io_type := [ [ "a", "b", "t", "s", "P", ], [ "P", "t_range" ] ], + input_arguments_names := [ "cat", "a", "b", "t", "s", "P" ], + output_source_getter_string := "P", + output_source_getter_preconditions := [ ], + output_range_getter_string := "Range( t )", + output_range_getter_preconditions := [ ], dual_operation := "UniversalMorphismIntoWeakBiFiberProductWithGivenWeakBiFiberProduct", pre_function := UNIVERSAL_MORPHISM_FROM_WEAK_BI_PUSHOUT_PREFUNCTION, return_type := "morphism", @@ -308,7 +368,7 @@ UniversalMorphismFromWeakBiPushoutWithGivenWeakBiPushout := rec( DirectSumMorphismToWeakBiPushout := rec( filter_list := [ "category", "morphism", "morphism" ], - io_type := [ [ "alpha", "beta" ], [ "S", "P" ] ], + input_arguments_names := [ "cat", "alpha", "beta" ], return_type := "morphism", dual_operation := "WeakBiFiberProductMorphismToDirectSum", ), @@ -324,7 +384,9 @@ BiasedWeakFiberProduct := rec( ProjectionOfBiasedWeakFiberProduct := rec( filter_list := [ "category", "morphism", "morphism" ], - io_type := [ [ "a", "b" ], [ "P", "a_source" ] ], + input_arguments_names := [ "cat", "a", "b" ], + output_range_getter_string := "Source( a )", + output_range_getter_preconditions := [ ], with_given_object_position := "Source", dual_operation := "InjectionOfBiasedWeakPushout", pre_function := WEAK_BI_FIBER_PRODUCT_PREFUNCTION, @@ -333,7 +395,11 @@ ProjectionOfBiasedWeakFiberProduct := rec( ProjectionOfBiasedWeakFiberProductWithGivenBiasedWeakFiberProduct := rec( filter_list := [ "category", "morphism", "morphism", "object" ], - io_type := [ [ "a", "b", "P" ], [ "P", "a_source" ] ], + input_arguments_names := [ "cat", "a", "b", "P" ], + output_source_getter_string := "P", + output_source_getter_preconditions := [ ], + output_range_getter_string := "Source( a )", + output_range_getter_preconditions := [ ], dual_operation := "InjectionOfBiasedWeakPushoutWithGivenBiasedWeakPushout", pre_function := WEAK_BI_FIBER_PRODUCT_PREFUNCTION, return_type := "morphism", @@ -341,7 +407,9 @@ ProjectionOfBiasedWeakFiberProductWithGivenBiasedWeakFiberProduct := rec( UniversalMorphismIntoBiasedWeakFiberProduct := rec( filter_list := [ "category", "morphism", "morphism", "morphism" ], - io_type := [ [ "a", "b", "t" ], [ "t_source", "P" ] ], + input_arguments_names := [ "cat", "a", "b", "t" ], + output_source_getter_string := "Source( t )", + output_source_getter_preconditions := [ ], with_given_object_position := "Range", dual_operation := "UniversalMorphismFromBiasedWeakPushout", pre_function := UNIVERSAL_MORPHISM_INTO_BIASED_WEAK_FIBER_PRODUCT_PREFUNCTION, @@ -350,7 +418,11 @@ UniversalMorphismIntoBiasedWeakFiberProduct := rec( UniversalMorphismIntoBiasedWeakFiberProductWithGivenBiasedWeakFiberProduct := rec( filter_list := [ "category", "morphism", "morphism", "morphism", "object" ], - io_type := [ [ "a", "b", "t", "P", ], [ "t_source", "P" ] ], + input_arguments_names := [ "cat", "a", "b", "t", "P" ], + output_source_getter_string := "Source( t )", + output_source_getter_preconditions := [ ], + output_range_getter_string := "P", + output_range_getter_preconditions := [ ], dual_operation := "UniversalMorphismFromBiasedWeakPushoutWithGivenBiasedWeakPushout", pre_function := UNIVERSAL_MORPHISM_INTO_BIASED_WEAK_FIBER_PRODUCT_PREFUNCTION, return_type := "morphism", @@ -369,7 +441,9 @@ BiasedWeakPushout := rec( InjectionOfBiasedWeakPushout := rec( filter_list := [ "category", "morphism", "morphism" ], - io_type := [ [ "a", "b" ], [ "a_range", "P" ] ], + input_arguments_names := [ "cat", "a", "b" ], + output_source_getter_string := "Range( a )", + output_source_getter_preconditions := [ ], with_given_object_position := "Range", dual_operation := "ProjectionOfBiasedWeakFiberProduct", pre_function := WEAK_BI_PUSHOUT_PREFUNCTION, @@ -378,7 +452,11 @@ InjectionOfBiasedWeakPushout := rec( InjectionOfBiasedWeakPushoutWithGivenBiasedWeakPushout := rec( filter_list := [ "category", "morphism", "morphism", "object" ], - io_type := [ [ "a", "b", "P" ], [ "a_range", "P" ] ], + input_arguments_names := [ "cat", "a", "b", "P" ], + output_source_getter_string := "Range( a )", + output_source_getter_preconditions := [ ], + output_range_getter_string := "P", + output_range_getter_preconditions := [ ], dual_operation := "ProjectionOfBiasedWeakFiberProductWithGivenBiasedWeakFiberProduct", pre_function := WEAK_BI_PUSHOUT_PREFUNCTION, return_type := "morphism", @@ -386,7 +464,9 @@ InjectionOfBiasedWeakPushoutWithGivenBiasedWeakPushout := rec( UniversalMorphismFromBiasedWeakPushout := rec( filter_list := [ "category", "morphism", "morphism", "morphism" ], - io_type := [ [ "a", "b", "t" ], [ "P", "t_range" ] ], + input_arguments_names := [ "cat", "a", "b", "t" ], + output_range_getter_string := "Range( t )", + output_range_getter_preconditions := [ ], with_given_object_position := "Source", dual_operation := "UniversalMorphismIntoBiasedWeakFiberProduct", pre_function := UNIVERSAL_MORPHISM_FROM_BIASED_WEAK_PUSHOUT_PREFUNCTION, @@ -395,7 +475,11 @@ UniversalMorphismFromBiasedWeakPushout := rec( UniversalMorphismFromBiasedWeakPushoutWithGivenBiasedWeakPushout := rec( filter_list := [ "category", "morphism", "morphism", "morphism", "object" ], - io_type := [ [ "a", "b", "t", "P", ], [ "P", "t_range" ] ], + input_arguments_names := [ "cat", "a", "b", "t", "P" ], + output_source_getter_string := "P", + output_source_getter_preconditions := [ ], + output_range_getter_string := "Range( t )", + output_range_getter_preconditions := [ ], dual_operation := "UniversalMorphismIntoBiasedWeakFiberProductWithGivenBiasedWeakFiberProduct", pre_function := UNIVERSAL_MORPHISM_FROM_BIASED_WEAK_PUSHOUT_PREFUNCTION, return_type := "morphism", diff --git a/MonoidalCategories/PackageInfo.g b/MonoidalCategories/PackageInfo.g index 186ac65b8e..d6a30c178e 100644 --- a/MonoidalCategories/PackageInfo.g +++ b/MonoidalCategories/PackageInfo.g @@ -10,7 +10,7 @@ SetPackageInfo( rec( PackageName := "MonoidalCategories", Subtitle := "Monoidal and monoidal (co)closed categories", -Version := "2023.05-03", +Version := "2023.07-01", 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/MonoidalCategories/gap/AdditiveMonoidalCategoriesMethodRecord.gi b/MonoidalCategories/gap/AdditiveMonoidalCategoriesMethodRecord.gi index 169584ae1c..0c4bbf8f2c 100644 --- a/MonoidalCategories/gap/AdditiveMonoidalCategoriesMethodRecord.gi +++ b/MonoidalCategories/gap/AdditiveMonoidalCategoriesMethodRecord.gi @@ -8,7 +8,7 @@ InstallValue( DISTRIBUTIVE_MONOIDAL_CATEGORIES_METHOD_NAME_RECORD, rec( LeftDistributivityExpanding := rec( filter_list := [ "category", "object", "list_of_objects" ], - io_type := [ [ "a", "L" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "a", "L" ], output_source_getter_string := "TensorProductOnObjects( cat, a, DirectSum( cat, L ) )", output_source_getter_preconditions := [ [ "TensorProductOnObjects", 1 ], [ "DirectSum", 1 ] ], output_range_getter_string := "DirectSum( cat, List( L, summand -> TensorProductOnObjects( cat, a, summand ) ) )", @@ -22,7 +22,11 @@ LeftDistributivityExpanding := rec( LeftDistributivityExpandingWithGivenObjects := rec( filter_list := [ "category", "object", "object", "list_of_objects", "object" ], - io_type := [ [ "s", "a", "L", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "a", "L", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "LeftDistributivityFactoringWithGivenObjects", dual_with_given_objects_reversed := true, @@ -30,7 +34,7 @@ LeftDistributivityExpandingWithGivenObjects := rec( LeftDistributivityFactoring := rec( filter_list := [ "category", "object", "list_of_objects" ], - io_type := [ [ "a", "L" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "a", "L" ], output_source_getter_string := "DirectSum( cat, List( L, summand -> TensorProductOnObjects( cat, a, summand ) ) )", output_source_getter_preconditions := [ [ "DirectSum", 1 ], [ "TensorProductOnObjects", 2 ] ], output_range_getter_string := "TensorProductOnObjects( cat, a, DirectSum( cat, L ) )", @@ -44,7 +48,11 @@ LeftDistributivityFactoring := rec( LeftDistributivityFactoringWithGivenObjects := rec( filter_list := [ "category", "object", "object", "list_of_objects", "object" ], - io_type := [ [ "s", "a", "L", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "a", "L", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "LeftDistributivityExpandingWithGivenObjects", dual_with_given_objects_reversed := true, @@ -52,7 +60,7 @@ LeftDistributivityFactoringWithGivenObjects := rec( RightDistributivityExpanding := rec( filter_list := [ "category", "list_of_objects", "object" ], - io_type := [ [ "L", "a" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "L", "a" ], output_source_getter_string := "TensorProductOnObjects( cat, DirectSum( cat, L ), a )", output_source_getter_preconditions := [ [ "TensorProductOnObjects", 1 ], [ "DirectSum", 1 ] ], output_range_getter_string := "DirectSum( cat, List( L, summand -> TensorProductOnObjects( cat, summand, a ) ) )", @@ -66,7 +74,11 @@ RightDistributivityExpanding := rec( RightDistributivityExpandingWithGivenObjects := rec( filter_list := [ "category", "object", "list_of_objects", "object", "object" ], - io_type := [ [ "s", "L", "a", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "L", "a", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "RightDistributivityFactoringWithGivenObjects", dual_with_given_objects_reversed := true, @@ -74,7 +86,7 @@ RightDistributivityExpandingWithGivenObjects := rec( RightDistributivityFactoring := rec( filter_list := [ "category", "list_of_objects", "object" ], - io_type := [ [ "L", "a" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "L", "a" ], output_source_getter_string := "DirectSum( cat, List( L, summand -> TensorProductOnObjects( cat, summand, a ) ) )", output_source_getter_preconditions := [ [ "DirectSum", 1 ], [ "TensorProductOnObjects", 2 ] ], output_range_getter_string := "TensorProductOnObjects( cat, DirectSum( cat, L ), a )", @@ -88,7 +100,11 @@ RightDistributivityFactoring := rec( RightDistributivityFactoringWithGivenObjects := rec( filter_list := [ "category", "object", "list_of_objects", "object", "object" ], - io_type := [ [ "s", "L", "a", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "L", "a", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "RightDistributivityExpandingWithGivenObjects", dual_with_given_objects_reversed := true, diff --git a/MonoidalCategories/gap/BraidedMonoidalCategoriesMethodRecord.gi b/MonoidalCategories/gap/BraidedMonoidalCategoriesMethodRecord.gi index eb55325af1..31eff6bfb8 100644 --- a/MonoidalCategories/gap/BraidedMonoidalCategoriesMethodRecord.gi +++ b/MonoidalCategories/gap/BraidedMonoidalCategoriesMethodRecord.gi @@ -8,7 +8,7 @@ InstallValue( BRAIDED_MONOIDAL_CATEGORIES_METHOD_NAME_RECORD, rec( Braiding := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "a", "b" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "a", "b" ], output_source_getter_string := "TensorProductOnObjects( cat, a, b )", output_source_getter_preconditions := [ [ "TensorProductOnObjects", 1 ] ], output_range_getter_string := "TensorProductOnObjects( cat, b, a )", @@ -22,7 +22,11 @@ Braiding := rec( BraidingWithGivenTensorProducts := rec( filter_list := [ "category", "object", "object", "object", "object" ], - io_type := [ [ "s", "a", "b", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "a", "b", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "BraidingInverseWithGivenTensorProducts", dual_with_given_objects_reversed := true, @@ -30,7 +34,7 @@ BraidingWithGivenTensorProducts := rec( BraidingInverse := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "a", "b" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "a", "b" ], output_source_getter_string := "TensorProductOnObjects( cat, b, a )", output_source_getter_preconditions := [ [ "TensorProductOnObjects", 1 ] ], output_range_getter_string := "TensorProductOnObjects( cat, a, b )", @@ -44,7 +48,11 @@ BraidingInverse := rec( BraidingInverseWithGivenTensorProducts := rec( filter_list := [ "category", "object", "object", "object", "object" ], - io_type := [ [ "s", "a", "b", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "a", "b", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "BraidingWithGivenTensorProducts", dual_with_given_objects_reversed := true, diff --git a/MonoidalCategories/gap/ClosedMonoidalCategoriesMethodRecord.gi b/MonoidalCategories/gap/ClosedMonoidalCategoriesMethodRecord.gi index 1e61876198..ae1ffb5068 100644 --- a/MonoidalCategories/gap/ClosedMonoidalCategoriesMethodRecord.gi +++ b/MonoidalCategories/gap/ClosedMonoidalCategoriesMethodRecord.gi @@ -17,7 +17,7 @@ InternalHomOnObjects := rec( InternalHomOnMorphisms := rec( filter_list := [ "category", "morphism", "morphism" ], - io_type := [ [ "alpha", "beta" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "alpha", "beta" ], output_source_getter_string := "InternalHomOnObjects( cat, Range( alpha ), Source( beta ) )", output_source_getter_preconditions := [ [ "InternalHomOnObjects", 1 ] ], output_range_getter_string := "InternalHomOnObjects( cat, Source( alpha ), Range( beta ) )", @@ -31,7 +31,11 @@ InternalHomOnMorphisms := rec( InternalHomOnMorphismsWithGivenInternalHoms := rec( filter_list := [ "category", "object", "morphism", "morphism", "object" ], - io_type := [ [ "s", "alpha", "beta", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "alpha", "beta", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "InternalCoHomOnMorphismsWithGivenInternalCoHoms", dual_arguments_reversed := true, @@ -39,7 +43,9 @@ InternalHomOnMorphismsWithGivenInternalHoms := rec( EvaluationMorphism := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "a", "b" ], [ "s", "b" ] ], + input_arguments_names := [ "cat", "a", "b" ], + output_range_getter_string := "b", + output_range_getter_preconditions := [ ], output_source_getter_string := "TensorProductOnObjects( cat, InternalHomOnObjects( cat, a, b ), a )", output_source_getter_preconditions := [ [ "TensorProductOnObjects", 1 ], [ "InternalHomOnObjects", 1 ] ], output_range_getter_string := "b", @@ -52,7 +58,11 @@ EvaluationMorphism := rec( EvaluationMorphismWithGivenSource := rec( filter_list := [ "category", "object", "object", "object" ], - io_type := [ [ "a", "b", "s" ], [ "s", "b" ] ], + input_arguments_names := [ "cat", "a", "b", "s" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "b", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "CoclosedEvaluationMorphismWithGivenRange", dual_preprocessor_func := { cat, a, b, s } -> NTuple( 4, Opposite( cat ), Opposite( b ), Opposite( a ), Opposite( s ) ), @@ -61,7 +71,9 @@ EvaluationMorphismWithGivenSource := rec( CoevaluationMorphism := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "a", "b" ], [ "a", "r" ] ], + input_arguments_names := [ "cat", "a", "b" ], + output_source_getter_string := "a", + output_source_getter_preconditions := [ ], output_source_getter_string := "a", output_range_getter_string := "InternalHomOnObjects( cat, b, TensorProductOnObjects( cat, a, b ) )", output_range_getter_preconditions := [ [ "InternalHomOnObjects", 1 ], [ "TensorProductOnObjects", 1 ] ], @@ -74,7 +86,11 @@ CoevaluationMorphism := rec( CoevaluationMorphismWithGivenRange := rec( filter_list := [ "category", "object", "object", "object" ], - io_type := [ [ "a", "b", "r" ], [ "a", "r" ] ], + input_arguments_names := [ "cat", "a", "b", "r" ], + output_source_getter_string := "a", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "CoclosedCoevaluationMorphismWithGivenSource", dual_arguments_reversed := false, @@ -82,7 +98,9 @@ CoevaluationMorphismWithGivenRange := rec( TensorProductToInternalHomAdjunctionMap := rec( filter_list := [ "category", "object", "object", "morphism" ], - io_type := [ [ "a", "b", "f" ], [ "a", "i" ] ], + input_arguments_names := [ "cat", "a", "b", "f" ], + output_source_getter_string := "a", + output_source_getter_preconditions := [ ], return_type := "morphism", dual_operation := "TensorProductToInternalCoHomAdjunctionMap", dual_arguments_reversed := false, @@ -91,7 +109,11 @@ TensorProductToInternalHomAdjunctionMap := rec( TensorProductToInternalHomAdjunctionMapWithGivenInternalHom := rec( filter_list := [ "category", "object", "object", "morphism", "object" ], - io_type := [ [ "a", "b", "f", "i" ], [ "a", "i" ] ], + input_arguments_names := [ "cat", "a", "b", "f", "i" ], + output_source_getter_string := "a", + output_source_getter_preconditions := [ ], + output_range_getter_string := "i", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "TensorProductToInternalCoHomAdjunctionMapWithGivenInternalCoHom", dual_arguments_reversed := false, @@ -99,7 +121,9 @@ TensorProductToInternalHomAdjunctionMapWithGivenInternalHom := rec( InternalHomToTensorProductAdjunctionMap := rec( filter_list := [ "category", "object", "object", "morphism" ], - io_type := [ [ "b", "c", "g" ], [ "t", "c" ] ], + input_arguments_names := [ "cat", "b", "c", "g" ], + output_range_getter_string := "c", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "InternalCoHomToTensorProductAdjunctionMap", dual_preprocessor_func := { cat, a, b, g } -> NTuple( 4, Opposite( cat ), Opposite( b ), Opposite( a ), Opposite( g ) ), @@ -109,7 +133,11 @@ InternalHomToTensorProductAdjunctionMap := rec( InternalHomToTensorProductAdjunctionMapWithGivenTensorProduct := rec( filter_list := [ "category", "object", "object", "morphism", "object" ], - io_type := [ [ "b", "c", "g", "t" ], [ "t", "c" ] ], + input_arguments_names := [ "cat", "b", "c", "g", "t" ], + output_source_getter_string := "t", + output_source_getter_preconditions := [ ], + output_range_getter_string := "c", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "InternalCoHomToTensorProductAdjunctionMapWithGivenTensorProduct", dual_preprocessor_func := { cat, a, b, g, t } -> NTuple( 4, Opposite( cat ), Opposite( b ), Opposite( a ), Opposite( g ),Opposite( t ) ), @@ -118,7 +146,7 @@ InternalHomToTensorProductAdjunctionMapWithGivenTensorProduct := rec( MonoidalPreComposeMorphism := rec( filter_list := [ "category", "object", "object", "object" ], - io_type := [ [ "a", "b", "c" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "a", "b", "c" ], output_source_getter_string := "TensorProductOnObjects( cat, InternalHomOnObjects( cat, a, b ), InternalHomOnObjects( cat, b, c ) )", output_source_getter_preconditions := [ [ "TensorProductOnObjects", 1 ], [ "InternalHomOnObjects", 2 ] ], output_range_getter_string := "InternalHomOnObjects( cat, a, c )", @@ -132,7 +160,11 @@ MonoidalPreComposeMorphism := rec( MonoidalPreComposeMorphismWithGivenObjects := rec( filter_list := [ "category", "object", "object", "object", "object", "object" ], - io_type := [ [ "s", "a", "b", "c", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "a", "b", "c", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "MonoidalPreCoComposeMorphismWithGivenObjects", dual_arguments_reversed := true, @@ -140,7 +172,7 @@ MonoidalPreComposeMorphismWithGivenObjects := rec( MonoidalPostComposeMorphism := rec( filter_list := [ "category", "object", "object", "object" ], - io_type := [ [ "a", "b", "c" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "a", "b", "c" ], output_source_getter_string := "TensorProductOnObjects( cat, InternalHomOnObjects( cat, b, c ), InternalHomOnObjects( cat, a, b ) )", output_source_getter_preconditions := [ [ "TensorProductOnObjects", 1 ], [ "InternalHomOnObjects", 2 ] ], output_range_getter_string := "InternalHomOnObjects( cat, a, c )", @@ -154,7 +186,11 @@ MonoidalPostComposeMorphism := rec( MonoidalPostComposeMorphismWithGivenObjects := rec( filter_list := [ "category", "object", "object", "object", "object", "object" ], - io_type := [ [ "s", "a", "b", "c", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "a", "b", "c", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "MonoidalPostCoComposeMorphismWithGivenObjects", dual_arguments_reversed := true, @@ -170,7 +206,7 @@ DualOnObjects := rec( DualOnMorphisms := rec( filter_list := [ "category", "morphism" ], - io_type := [ [ "alpha" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "alpha" ], output_source_getter_string := "DualOnObjects( cat, Range( alpha ) )", output_source_getter_preconditions := [ [ "DualOnObjects", 1 ] ], output_range_getter_string := "DualOnObjects( cat, Source( alpha ) )", @@ -183,7 +219,11 @@ DualOnMorphisms := rec( DualOnMorphismsWithGivenDuals := rec( filter_list := [ "category", "object", "morphism", "object" ], - io_type := [ [ "s", "alpha", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "alpha", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "CoDualOnMorphismsWithGivenCoDuals", dual_arguments_reversed := true, @@ -191,7 +231,7 @@ DualOnMorphismsWithGivenDuals := rec( EvaluationForDual := rec( filter_list := [ "category", "object" ], - io_type := [ [ "a" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "a" ], output_source_getter_string := "TensorProductOnObjects( cat, DualOnObjects( cat, a ), a )", output_source_getter_preconditions := [ [ "TensorProductOnObjects", 1 ], [ "DualOnObjects", 1 ] ], output_range_getter_string := "TensorUnit( cat )", @@ -204,7 +244,11 @@ EvaluationForDual := rec( EvaluationForDualWithGivenTensorProduct := rec( filter_list := [ "category", "object", "object", "object" ], - io_type := [ [ "s", "a", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "a", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "CoclosedEvaluationForCoDualWithGivenTensorProduct", dual_arguments_reversed := true, @@ -212,7 +256,9 @@ EvaluationForDualWithGivenTensorProduct := rec( MorphismToBidual := rec( filter_list := [ "category", "object" ], - io_type := [ [ "a" ], [ "a", "r" ] ], + input_arguments_names := [ "cat", "a" ], + output_source_getter_string := "a", + output_source_getter_preconditions := [ ], output_source_getter_string := "a", output_range_getter_string := "DualOnObjects( cat, DualOnObjects( cat, a ) )", output_range_getter_preconditions := [ [ "DualOnObjects", 2 ] ], @@ -224,7 +270,11 @@ MorphismToBidual := rec( MorphismToBidualWithGivenBidual := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "a", "r" ], [ "a", "r" ] ], + input_arguments_names := [ "cat", "a", "r" ], + output_source_getter_string := "a", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "MorphismFromCoBidualWithGivenCoBidual", dual_arguments_reversed := false, @@ -259,7 +309,7 @@ TensorProductInternalHomCompatibilityMorphismWithGivenObjects := rec( TensorProductDualityCompatibilityMorphism := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "a", "b" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "a", "b" ], output_source_getter_string := "TensorProductOnObjects( cat, DualOnObjects( cat, a ), DualOnObjects( cat, b ) )", output_source_getter_preconditions := [ [ "TensorProductOnObjects", 1 ], [ "DualOnObjects", 2 ] ], output_range_getter_string := "DualOnObjects( cat, TensorProductOnObjects( cat, a, b ) )", @@ -273,7 +323,11 @@ TensorProductDualityCompatibilityMorphism := rec( TensorProductDualityCompatibilityMorphismWithGivenObjects := rec( filter_list := [ "category", "object", "object", "object", "object" ], - io_type := [ [ "s", "a", "b", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "a", "b", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "CoDualityTensorProductCompatibilityMorphismWithGivenObjects", dual_with_given_objects_reversed := true, @@ -281,7 +335,7 @@ TensorProductDualityCompatibilityMorphismWithGivenObjects := rec( MorphismFromTensorProductToInternalHom := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "a", "b" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "a", "b" ], output_source_getter_string := "TensorProductOnObjects( cat, DualOnObjects( cat, a ), b )", output_source_getter_preconditions := [ [ "TensorProductOnObjects", 1 ], [ "DualOnObjects", 1 ] ], output_range_getter_string := "InternalHomOnObjects( cat, a, b )", @@ -295,7 +349,11 @@ MorphismFromTensorProductToInternalHom := rec( MorphismFromTensorProductToInternalHomWithGivenObjects := rec( filter_list := [ "category", "object", "object", "object", "object" ], - io_type := [ [ "s", "a", "b", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "a", "b", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "MorphismFromInternalCoHomToTensorProductWithGivenObjects", dual_arguments_reversed := true, @@ -303,7 +361,7 @@ MorphismFromTensorProductToInternalHomWithGivenObjects := rec( IsomorphismFromInternalHomIntoTensorUnitToDualObject := rec( filter_list := [ "category", "object" ], - io_type := [ [ "a" ], [ "i", "d" ] ], + input_arguments_names := [ "cat", "a" ], output_source_getter_string := "InternalHomOnObjects( cat, a, TensorUnit( cat ) )", output_source_getter_preconditions := [ [ "InternalHomOnObjects", 1 ], [ "TensorUnit", 1 ] ], output_range_getter_string := "DualOnObjects( cat, a )", @@ -315,7 +373,7 @@ IsomorphismFromInternalHomIntoTensorUnitToDualObject := rec( IsomorphismFromDualObjectToInternalHomIntoTensorUnit := rec( filter_list := [ "category", "object" ], - io_type := [ [ "a" ], [ "d", "i" ] ], + input_arguments_names := [ "cat", "a" ], output_source_getter_string := "DualOnObjects( cat, a )", output_source_getter_preconditions := [ [ "DualOnObjects", 1 ] ], output_range_getter_string := "InternalHomOnObjects( cat, a, TensorUnit( cat ) )", @@ -327,7 +385,9 @@ IsomorphismFromDualObjectToInternalHomIntoTensorUnit := rec( UniversalPropertyOfDual := rec( filter_list := [ "category", "object", "object", "morphism" ], - io_type := [ [ "t", "a", "alpha" ], [ "t", "d" ] ], + input_arguments_names := [ "cat", "t", "a", "alpha" ], + output_source_getter_string := "t", + output_source_getter_preconditions := [ ], return_type := "morphism", dual_operation := "UniversalPropertyOfCoDual", dual_arguments_reversed := false, @@ -336,7 +396,7 @@ UniversalPropertyOfDual := rec( LambdaIntroduction := rec( filter_list := [ "category", "morphism" ], - io_type := [ [ "alpha" ], [ "u", "i" ] ], + input_arguments_names := [ "cat", "alpha" ], return_type := "morphism", dual_operation := "CoLambdaIntroduction", # Test in ClosedMonoidalCategoriesTest @@ -344,7 +404,11 @@ LambdaIntroduction := rec( LambdaElimination := rec( filter_list := [ "category", "object", "object", "morphism" ], - io_type := [ [ "a", "b", "alpha" ], [ "a", "b" ] ], + input_arguments_names := [ "cat", "a", "b", "alpha" ], + output_source_getter_string := "a", + output_source_getter_preconditions := [ ], + output_range_getter_string := "b", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "CoLambdaElimination", dual_preprocessor_func := { cat, a, b, alpha } -> NTuple( 4, Opposite( cat ), Opposite( b ), Opposite( a ), Opposite( alpha ) ), @@ -354,7 +418,9 @@ LambdaElimination := rec( IsomorphismFromObjectToInternalHom := rec( filter_list := [ "category", "object" ], - io_type := [ [ "a" ], [ "a", "r" ] ], + input_arguments_names := [ "cat", "a" ], + output_source_getter_string := "a", + output_source_getter_preconditions := [ ], output_source_getter_string := "a", output_range_getter_string := "InternalHomOnObjects( cat, TensorUnit( cat ), a )", output_range_getter_preconditions := [ [ "InternalHomOnObjects", 1 ], [ "TensorUnit", 1 ] ], @@ -366,7 +432,11 @@ IsomorphismFromObjectToInternalHom := rec( IsomorphismFromObjectToInternalHomWithGivenInternalHom := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "a", "r" ], [ "a", "r" ] ], + input_arguments_names := [ "cat", "a", "r" ], + output_source_getter_string := "a", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "IsomorphismFromInternalCoHomToObjectWithGivenInternalCoHom", dual_arguments_reversed := false, @@ -374,7 +444,9 @@ IsomorphismFromObjectToInternalHomWithGivenInternalHom := rec( IsomorphismFromInternalHomToObject := rec( filter_list := [ "category", "object" ], - io_type := [ [ "a" ], [ "s", "a" ] ], + input_arguments_names := [ "cat", "a" ], + output_range_getter_string := "a", + output_range_getter_preconditions := [ ], output_source_getter_string := "InternalHomOnObjects( cat, TensorUnit( cat ), a )", output_source_getter_preconditions := [ [ "InternalHomOnObjects", 1 ], [ "TensorUnit", 1 ] ], output_range_getter_string := "a", @@ -386,7 +458,11 @@ IsomorphismFromInternalHomToObject := rec( IsomorphismFromInternalHomToObjectWithGivenInternalHom := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "a", "s" ], [ "s", "a" ] ], + input_arguments_names := [ "cat", "a", "s" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "a", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "IsomorphismFromObjectToInternalCoHomWithGivenInternalCoHom", dual_arguments_reversed := false, diff --git a/MonoidalCategories/gap/CoclosedMonoidalCategoriesMethodRecord.gi b/MonoidalCategories/gap/CoclosedMonoidalCategoriesMethodRecord.gi index cecdead765..c33e73dbb1 100644 --- a/MonoidalCategories/gap/CoclosedMonoidalCategoriesMethodRecord.gi +++ b/MonoidalCategories/gap/CoclosedMonoidalCategoriesMethodRecord.gi @@ -17,7 +17,7 @@ InternalCoHomOnObjects := rec( InternalCoHomOnMorphisms := rec( filter_list := [ "category", "morphism", "morphism" ], - io_type := [ [ "alpha", "beta" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "alpha", "beta" ], output_source_getter_string := "InternalCoHomOnObjects( cat, Source( alpha ), Range( beta ) )", output_source_getter_preconditions := [ [ "InternalCoHomOnObjects", 1 ] ], output_range_getter_string := "InternalCoHomOnObjects( cat, Range( alpha ), Source( beta ) )", @@ -31,7 +31,11 @@ InternalCoHomOnMorphisms := rec( InternalCoHomOnMorphismsWithGivenInternalCoHoms := rec( filter_list := [ "category", "object", "morphism", "morphism", "object" ], - io_type := [ [ "s", "alpha", "beta", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "alpha", "beta", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "InternalHomOnMorphismsWithGivenInternalHoms", dual_arguments_reversed := true, @@ -39,7 +43,9 @@ InternalCoHomOnMorphismsWithGivenInternalCoHoms := rec( CoclosedEvaluationMorphism := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "a", "b" ], [ "a", "r" ] ], + input_arguments_names := [ "cat", "a", "b" ], + output_source_getter_string := "a", + output_source_getter_preconditions := [ ], output_source_getter_string := "a", output_range_getter_string := "TensorProductOnObjects( cat, InternalCoHomOnObjects( cat, a, b ), b )", output_range_getter_preconditions := [ [ "TensorProductOnObjects", 1 ], [ "InternalCoHomOnObjects", 1 ] ], @@ -52,7 +58,11 @@ CoclosedEvaluationMorphism := rec( CoclosedEvaluationMorphismWithGivenRange := rec( filter_list := [ "category", "object", "object", "object" ], - io_type := [ [ "a", "b", "r" ], [ "a", "r" ] ], + input_arguments_names := [ "cat", "a", "b", "r" ], + output_source_getter_string := "a", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "EvaluationMorphismWithGivenSource", dual_preprocessor_func := { cat, a, b, r } -> NTuple( 4, Opposite( cat ), Opposite( b ), Opposite( a ), Opposite( r ) ), @@ -61,7 +71,9 @@ CoclosedEvaluationMorphismWithGivenRange := rec( CoclosedCoevaluationMorphism := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "a", "b" ], [ "s", "a" ] ], + input_arguments_names := [ "cat", "a", "b" ], + output_range_getter_string := "a", + output_range_getter_preconditions := [ ], output_source_getter_string := "InternalCoHomOnObjects( cat, TensorProductOnObjects( cat, a, b ), b )", output_source_getter_preconditions := [ [ "InternalCoHomOnObjects", 1 ], [ "TensorProductOnObjects", 1 ] ], output_range_getter_string := "a", @@ -74,7 +86,11 @@ CoclosedCoevaluationMorphism := rec( CoclosedCoevaluationMorphismWithGivenSource := rec( filter_list := [ "category", "object", "object", "object" ], - io_type := [ [ "a", "b", "s" ], [ "s", "a" ] ], + input_arguments_names := [ "cat", "a", "b", "s" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "a", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "CoevaluationMorphismWithGivenRange", dual_arguments_reversed := false, @@ -82,7 +98,9 @@ CoclosedCoevaluationMorphismWithGivenSource := rec( TensorProductToInternalCoHomAdjunctionMap := rec( filter_list := [ "category", "object", "object", "morphism" ], - io_type := [ [ "c", "b", "g" ], [ "i", "c" ] ], + input_arguments_names := [ "cat", "c", "b", "g" ], + output_range_getter_string := "c", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "TensorProductToInternalHomAdjunctionMap", dual_arguments_reversed := false, @@ -91,7 +109,11 @@ TensorProductToInternalCoHomAdjunctionMap := rec( TensorProductToInternalCoHomAdjunctionMapWithGivenInternalCoHom := rec( filter_list := [ "category", "object", "object", "morphism", "object" ], - io_type := [ [ "c", "b", "g", "i" ], [ "i", "c" ] ], + input_arguments_names := [ "cat", "c", "b", "g", "i" ], + output_source_getter_string := "i", + output_source_getter_preconditions := [ ], + output_range_getter_string := "c", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "TensorProductToInternalHomAdjunctionMapWithGivenInternalHom", dual_arguments_reversed := false, @@ -99,7 +121,9 @@ TensorProductToInternalCoHomAdjunctionMapWithGivenInternalCoHom := rec( InternalCoHomToTensorProductAdjunctionMap := rec( filter_list := [ "category", "object", "object", "morphism" ], - io_type := [ [ "a", "b", "f", ], [ "a", "t" ] ], + input_arguments_names := [ "cat", "a", "b", "f" ], + output_source_getter_string := "a", + output_source_getter_preconditions := [ ], return_type := "morphism", dual_operation := "InternalHomToTensorProductAdjunctionMap", dual_preprocessor_func := { cat, a, b, f } -> NTuple( 4, Opposite( cat ), Opposite( b ), Opposite( a ), Opposite( f ) ), @@ -109,7 +133,11 @@ InternalCoHomToTensorProductAdjunctionMap := rec( InternalCoHomToTensorProductAdjunctionMapWithGivenTensorProduct := rec( filter_list := [ "category", "object", "object", "morphism", "object" ], - io_type := [ [ "a", "b", "f", "t" ], [ "a", "t" ] ], + input_arguments_names := [ "cat", "a", "b", "f", "t" ], + output_source_getter_string := "a", + output_source_getter_preconditions := [ ], + output_range_getter_string := "t", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "InternalHomToTensorProductAdjunctionMapWithGivenTensorProduct", dual_preprocessor_func := { cat, a, b, f, t } -> NTuple( 4, Opposite( cat ), Opposite( b ), Opposite( a ), Opposite( f ), Opposite( t ) ), @@ -118,7 +146,7 @@ InternalCoHomToTensorProductAdjunctionMapWithGivenTensorProduct := rec( MonoidalPreCoComposeMorphism := rec( filter_list := [ "category", "object", "object", "object" ], - io_type := [ [ "a", "b", "c" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "a", "b", "c" ], output_source_getter_string := "InternalCoHomOnObjects( cat, a, c )", output_source_getter_preconditions := [ [ "InternalCoHomOnObjects", 1 ] ], output_range_getter_string := "TensorProductOnObjects( cat, InternalCoHomOnObjects( cat, b, c ), InternalCoHomOnObjects( cat, a, b ) )", @@ -132,7 +160,11 @@ MonoidalPreCoComposeMorphism := rec( MonoidalPreCoComposeMorphismWithGivenObjects := rec( filter_list := [ "category", "object", "object", "object", "object", "object" ], - io_type := [ [ "s", "a", "b", "c", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "a", "b", "c", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "MonoidalPreComposeMorphismWithGivenObjects", dual_arguments_reversed := true, @@ -140,7 +172,7 @@ MonoidalPreCoComposeMorphismWithGivenObjects := rec( MonoidalPostCoComposeMorphism := rec( filter_list := [ "category", "object", "object", "object" ], - io_type := [ [ "a", "b", "c" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "a", "b", "c" ], output_source_getter_string := "InternalCoHomOnObjects( cat, a, c )", output_source_getter_preconditions := [ [ "InternalCoHomOnObjects", 1 ] ], output_range_getter_string := "TensorProductOnObjects( cat, InternalCoHomOnObjects( cat, a, b ), InternalCoHomOnObjects( cat, b, c ) )", @@ -154,7 +186,11 @@ MonoidalPostCoComposeMorphism := rec( MonoidalPostCoComposeMorphismWithGivenObjects := rec( filter_list := [ "category", "object", "object", "object", "object", "object" ], - io_type := [ [ "s", "a", "b", "c", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "a", "b", "c", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "MonoidalPostComposeMorphismWithGivenObjects", dual_arguments_reversed := true, @@ -170,7 +206,7 @@ CoDualOnObjects := rec( CoDualOnMorphisms := rec( filter_list := [ "category", "morphism" ], - io_type := [ [ "alpha" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "alpha" ], output_source_getter_string := "CoDualOnObjects( cat, Range( alpha ) )", output_source_getter_preconditions := [ [ "CoDualOnObjects", 1 ] ], output_range_getter_string := "CoDualOnObjects( cat, Source( alpha ) )", @@ -183,7 +219,11 @@ CoDualOnMorphisms := rec( CoDualOnMorphismsWithGivenCoDuals := rec( filter_list := [ "category", "object", "morphism", "object" ], - io_type := [ [ "s", "alpha", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "alpha", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "DualOnMorphismsWithGivenDuals", dual_arguments_reversed := true, @@ -191,7 +231,7 @@ CoDualOnMorphismsWithGivenCoDuals := rec( CoclosedEvaluationForCoDual := rec( filter_list := [ "category", "object" ], - io_type := [ [ "a" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "a" ], output_source_getter_string := "TensorUnit( cat )", output_source_getter_preconditions := [ [ "TensorUnit", 1 ] ], output_range_getter_string := "TensorProductOnObjects( cat, CoDualOnObjects( cat, a ), a )", @@ -204,7 +244,11 @@ CoclosedEvaluationForCoDual := rec( CoclosedEvaluationForCoDualWithGivenTensorProduct := rec( filter_list := [ "category", "object", "object", "object" ], - io_type := [ [ "s", "a", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "a", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "EvaluationForDualWithGivenTensorProduct", dual_arguments_reversed := true, @@ -212,7 +256,9 @@ CoclosedEvaluationForCoDualWithGivenTensorProduct := rec( MorphismFromCoBidual := rec( filter_list := [ "category", "object" ], - io_type := [ [ "a" ], [ "s", "a" ] ], + input_arguments_names := [ "cat", "a" ], + output_range_getter_string := "a", + output_range_getter_preconditions := [ ], output_source_getter_string := "CoDualOnObjects( cat, CoDualOnObjects( cat, a ) )", output_source_getter_preconditions := [ [ "CoDualOnObjects", 2 ] ], output_range_getter_string := "a", @@ -224,7 +270,11 @@ MorphismFromCoBidual := rec( MorphismFromCoBidualWithGivenCoBidual := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "a", "s" ], [ "s", "a" ] ], + input_arguments_names := [ "cat", "a", "s" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "a", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "MorphismToBidualWithGivenBidual", dual_arguments_reversed := false, @@ -259,7 +309,7 @@ InternalCoHomTensorProductCompatibilityMorphismWithGivenObjects := rec( CoDualityTensorProductCompatibilityMorphism := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "a", "b" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "a", "b" ], output_source_getter_string := "CoDualOnObjects( cat, TensorProductOnObjects( cat, a, b ) )", output_source_getter_preconditions := [ [ "CoDualOnObjects", 1 ], [ "TensorProductOnObjects", 1 ] ], output_range_getter_string := "TensorProductOnObjects( cat, CoDualOnObjects( cat, a ), CoDualOnObjects( cat, b ) )", @@ -273,7 +323,11 @@ CoDualityTensorProductCompatibilityMorphism := rec( CoDualityTensorProductCompatibilityMorphismWithGivenObjects := rec( filter_list := [ "category", "object", "object", "object", "object" ], - io_type := [ [ "s", "a", "b", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "a", "b", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "TensorProductDualityCompatibilityMorphismWithGivenObjects", dual_with_given_objects_reversed := true, @@ -281,7 +335,7 @@ CoDualityTensorProductCompatibilityMorphismWithGivenObjects := rec( MorphismFromInternalCoHomToTensorProduct := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "a", "b" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "a", "b" ], output_source_getter_string := "InternalCoHomOnObjects( cat, a, b )", output_source_getter_preconditions := [ [ "InternalCoHomOnObjects", 1 ] ], output_range_getter_string := "TensorProductOnObjects( cat, CoDualOnObjects( cat, b ), a )", @@ -295,7 +349,11 @@ MorphismFromInternalCoHomToTensorProduct := rec( MorphismFromInternalCoHomToTensorProductWithGivenObjects := rec( filter_list := [ "category", "object", "object", "object", "object" ], - io_type := [ [ "s", "a", "b", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "a", "b", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "MorphismFromTensorProductToInternalHomWithGivenObjects", dual_arguments_reversed := true, @@ -303,7 +361,7 @@ MorphismFromInternalCoHomToTensorProductWithGivenObjects := rec( IsomorphismFromCoDualObjectToInternalCoHomFromTensorUnit := rec( filter_list := [ "category", "object" ], - io_type := [ [ "a" ], [ "d", "i" ] ], + input_arguments_names := [ "cat", "a" ], output_source_getter_string := "CoDualOnObjects( cat, a )", output_source_getter_preconditions := [ [ "CoDualOnObjects", 1 ] ], output_range_getter_string := "InternalCoHomOnObjects( cat, TensorUnit( cat ), a )", @@ -315,7 +373,7 @@ IsomorphismFromCoDualObjectToInternalCoHomFromTensorUnit := rec( IsomorphismFromInternalCoHomFromTensorUnitToCoDualObject := rec( filter_list := [ "category", "object" ], - io_type := [ [ "a" ], [ "i", "d" ] ], + input_arguments_names := [ "cat", "a" ], output_source_getter_string := "InternalCoHomOnObjects( cat, TensorUnit( cat ), a )", output_source_getter_preconditions := [ [ "InternalCoHomOnObjects", 1 ], [ "TensorUnit", 1 ] ], output_range_getter_string := "CoDualOnObjects( cat, a )", @@ -327,7 +385,9 @@ IsomorphismFromInternalCoHomFromTensorUnitToCoDualObject := rec( UniversalPropertyOfCoDual := rec( filter_list := [ "category", "object", "object", "morphism" ], - io_type := [ [ "t", "a", "alpha" ], [ "d", "t" ] ], + input_arguments_names := [ "cat", "t", "a", "alpha" ], + output_range_getter_string := "t", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "UniversalPropertyOfDual", dual_arguments_reversed := false, @@ -336,7 +396,7 @@ UniversalPropertyOfCoDual := rec( CoLambdaIntroduction := rec( filter_list := [ "category", "morphism" ], - io_type := [ [ "alpha" ], [ "u", "i" ] ], + input_arguments_names := [ "cat", "alpha" ], return_type := "morphism", dual_operation := "LambdaIntroduction", # Test in CoclosedMonoidalCategoriesTest @@ -344,7 +404,11 @@ CoLambdaIntroduction := rec( CoLambdaElimination := rec( filter_list := [ "category", "object", "object", "morphism" ], - io_type := [ [ "a", "b", "alpha" ], [ "a", "b" ] ], + input_arguments_names := [ "cat", "a", "b", "alpha" ], + output_source_getter_string := "a", + output_source_getter_preconditions := [ ], + output_range_getter_string := "b", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "LambdaElimination", dual_preprocessor_func := { cat, a, b, alpha } -> NTuple( 4, Opposite( cat ), Opposite( b ), Opposite( a ), Opposite( alpha ) ), @@ -354,7 +418,9 @@ CoLambdaElimination := rec( IsomorphismFromObjectToInternalCoHom := rec( filter_list := [ "category", "object" ], - io_type := [ [ "a" ], [ "a", "r" ] ], + input_arguments_names := [ "cat", "a" ], + output_source_getter_string := "a", + output_source_getter_preconditions := [ ], output_source_getter_string := "a", output_range_getter_string := "InternalCoHomOnObjects( cat, a, TensorUnit( cat ) )", output_range_getter_preconditions := [ [ "InternalCoHomOnObjects", 1 ], [ "TensorUnit", 1 ] ], @@ -366,7 +432,11 @@ IsomorphismFromObjectToInternalCoHom := rec( IsomorphismFromObjectToInternalCoHomWithGivenInternalCoHom := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "a", "r" ], [ "a", "r" ] ], + input_arguments_names := [ "cat", "a", "r" ], + output_source_getter_string := "a", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "IsomorphismFromInternalHomToObjectWithGivenInternalHom", dual_arguments_reversed := false, @@ -374,7 +444,9 @@ IsomorphismFromObjectToInternalCoHomWithGivenInternalCoHom := rec( IsomorphismFromInternalCoHomToObject := rec( filter_list := [ "category", "object" ], - io_type := [ [ "a" ], [ "s", "a" ] ], + input_arguments_names := [ "cat", "a" ], + output_range_getter_string := "a", + output_range_getter_preconditions := [ ], output_source_getter_string := "InternalCoHomOnObjects( cat, a, TensorUnit( cat ) )", output_source_getter_preconditions := [ [ "InternalCoHomOnObjects", 1 ], [ "TensorUnit", 1 ] ], output_range_getter_string := "a", @@ -386,7 +458,11 @@ IsomorphismFromInternalCoHomToObject := rec( IsomorphismFromInternalCoHomToObjectWithGivenInternalCoHom := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "a", "s" ], [ "s", "a" ] ], + input_arguments_names := [ "cat", "a", "s" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "a", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "IsomorphismFromObjectToInternalHomWithGivenInternalHom", dual_arguments_reversed := false, diff --git a/MonoidalCategories/gap/MonoidalCategoriesMethodRecord.gi b/MonoidalCategories/gap/MonoidalCategoriesMethodRecord.gi index 51e3bc0213..3c0b7db7ab 100644 --- a/MonoidalCategories/gap/MonoidalCategoriesMethodRecord.gi +++ b/MonoidalCategories/gap/MonoidalCategoriesMethodRecord.gi @@ -10,7 +10,7 @@ InstallValue( MONOIDAL_CATEGORIES_METHOD_NAME_RECORD, rec( TensorProductOnMorphisms := rec( filter_list := [ "category", "morphism", "morphism" ], - io_type := [ [ "alpha", "beta" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "alpha", "beta" ], output_source_getter_string := "TensorProductOnObjects( cat, Source( alpha ), Source( beta ) )", output_source_getter_preconditions := [ [ "TensorProductOnObjects", 1 ] ], output_range_getter_string := "TensorProductOnObjects( cat, Range( alpha ), Range( beta ) )", @@ -25,7 +25,11 @@ TensorProductOnMorphisms := rec( TensorProductOnMorphismsWithGivenTensorProducts := rec( filter_list := [ "category", "object", "morphism", "morphism", "object" ], - io_type := [ [ "s", "alpha", "beta", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "alpha", "beta", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "TensorProductOnMorphismsWithGivenTensorProducts", dual_with_given_objects_reversed := true, @@ -34,7 +38,7 @@ TensorProductOnMorphismsWithGivenTensorProducts := rec( AssociatorRightToLeft := rec( filter_list := [ "category", "object", "object", "object" ], - io_type := [ [ "a", "b", "c" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "a", "b", "c" ], output_source_getter_string := "TensorProductOnObjects( cat, a, TensorProductOnObjects( cat, b, c ) )", output_source_getter_preconditions := [ [ "TensorProductOnObjects", 2 ] ], output_range_getter_string := "TensorProductOnObjects( cat, TensorProductOnObjects( cat, a, b ), c )", @@ -48,7 +52,11 @@ AssociatorRightToLeft := rec( AssociatorRightToLeftWithGivenTensorProducts := rec( filter_list := [ "category", "object", "object", "object", "object", "object" ], - io_type := [ [ "s", "a", "b", "c", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "a", "b", "c", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "AssociatorLeftToRightWithGivenTensorProducts", dual_with_given_objects_reversed := true, @@ -56,7 +64,7 @@ AssociatorRightToLeftWithGivenTensorProducts := rec( AssociatorLeftToRight := rec( filter_list := [ "category", "object", "object", "object" ], - io_type := [ [ "a", "b", "c" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "a", "b", "c" ], output_source_getter_string := "TensorProductOnObjects( cat, TensorProductOnObjects( cat, a, b ), c )", output_source_getter_preconditions := [ [ "TensorProductOnObjects", 2 ] ], output_range_getter_string := "TensorProductOnObjects( cat, a, TensorProductOnObjects( cat, b, c ) )", @@ -70,7 +78,11 @@ AssociatorLeftToRight := rec( AssociatorLeftToRightWithGivenTensorProducts := rec( filter_list := [ "category", "object", "object", "object", "object", "object" ], - io_type := [ [ "s", "a", "b", "c", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "a", "b", "c", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "AssociatorRightToLeftWithGivenTensorProducts", dual_with_given_objects_reversed := true, @@ -78,7 +90,9 @@ AssociatorLeftToRightWithGivenTensorProducts := rec( LeftUnitor := rec( filter_list := [ "category", "object" ], - io_type := [ [ "a" ], [ "s", "a" ] ], + input_arguments_names := [ "cat", "a" ], + output_range_getter_string := "a", + output_range_getter_preconditions := [ ], output_source_getter_string := "TensorProductOnObjects( cat, TensorUnit( cat ), a )", output_source_getter_preconditions := [ [ "TensorProductOnObjects", 1 ], [ "TensorUnit", 1 ] ], output_range_getter_string := "a", @@ -90,7 +104,11 @@ LeftUnitor := rec( LeftUnitorWithGivenTensorProduct := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "a", "s" ], [ "s", "a" ] ], + input_arguments_names := [ "cat", "a", "s" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "a", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "LeftUnitorInverseWithGivenTensorProduct", dual_arguments_reversed := false, @@ -98,7 +116,9 @@ LeftUnitorWithGivenTensorProduct := rec( LeftUnitorInverse := rec( filter_list := [ "category", "object" ], - io_type := [ [ "a" ], [ "a", "r" ] ], + input_arguments_names := [ "cat", "a" ], + output_source_getter_string := "a", + output_source_getter_preconditions := [ ], output_source_getter_string := "a", output_range_getter_string := "TensorProductOnObjects( cat, TensorUnit( cat ), a )", output_range_getter_preconditions := [ [ "TensorProductOnObjects", 1 ], [ "TensorUnit", 1 ] ], @@ -110,7 +130,11 @@ LeftUnitorInverse := rec( LeftUnitorInverseWithGivenTensorProduct := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "a", "r" ], [ "a", "r" ] ], + input_arguments_names := [ "cat", "a", "r" ], + output_source_getter_string := "a", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "LeftUnitorWithGivenTensorProduct", dual_arguments_reversed := false, @@ -118,7 +142,9 @@ LeftUnitorInverseWithGivenTensorProduct := rec( RightUnitor := rec( filter_list := [ "category", "object" ], - io_type := [ [ "a" ], [ "s", "a" ] ], + input_arguments_names := [ "cat", "a" ], + output_range_getter_string := "a", + output_range_getter_preconditions := [ ], output_source_getter_string := "TensorProductOnObjects( cat, a, TensorUnit( cat ) )", output_source_getter_preconditions := [ [ "TensorProductOnObjects", 1 ], [ "TensorUnit", 1 ] ], output_range_getter_string := "a", @@ -130,7 +156,11 @@ RightUnitor := rec( RightUnitorWithGivenTensorProduct := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "a", "s" ], [ "s", "a" ] ], + input_arguments_names := [ "cat", "a", "s" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "a", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "RightUnitorInverseWithGivenTensorProduct", dual_arguments_reversed := false, @@ -138,7 +168,9 @@ RightUnitorWithGivenTensorProduct := rec( RightUnitorInverse := rec( filter_list := [ "category", "object" ], - io_type := [ [ "a" ], [ "a", "r" ] ], + input_arguments_names := [ "cat", "a" ], + output_source_getter_string := "a", + output_source_getter_preconditions := [ ], output_source_getter_string := "a", output_range_getter_string := "TensorProductOnObjects( cat, a, TensorUnit( cat ) )", output_range_getter_preconditions := [ [ "TensorProductOnObjects", 1 ], [ "TensorUnit", 1 ] ], @@ -150,7 +182,11 @@ RightUnitorInverse := rec( RightUnitorInverseWithGivenTensorProduct := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "a", "r" ], [ "a", "r" ] ], + input_arguments_names := [ "cat", "a", "r" ], + output_source_getter_string := "a", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "RightUnitorWithGivenTensorProduct", dual_arguments_reversed := false, diff --git a/MonoidalCategories/gap/RigidSymmetricClosedMonoidalCategoriesMethodRecord.gi b/MonoidalCategories/gap/RigidSymmetricClosedMonoidalCategoriesMethodRecord.gi index 1974586b90..083edec6e7 100644 --- a/MonoidalCategories/gap/RigidSymmetricClosedMonoidalCategoriesMethodRecord.gi +++ b/MonoidalCategories/gap/RigidSymmetricClosedMonoidalCategoriesMethodRecord.gi @@ -8,7 +8,7 @@ InstallValue( RIGID_SYMMETRIC_CLOSED_MONOIDAL_CATEGORIES_METHOD_NAME_RECORD, rec CoevaluationForDual := rec( filter_list := [ "category", "object" ], - io_type := [ [ "a" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "a" ], output_source_getter_string := "TensorUnit( cat )", output_source_getter_preconditions := [ [ "TensorUnit", 1 ] ], output_range_getter_string := "TensorProductOnObjects( cat, a, DualOnObjects( cat, a ) )", @@ -21,7 +21,11 @@ CoevaluationForDual := rec( CoevaluationForDualWithGivenTensorProduct := rec( filter_list := [ "category", "object", "object", "object" ], - io_type := [ [ "s", "a", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "a", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "CoclosedCoevaluationForCoDualWithGivenTensorProduct", dual_arguments_reversed := true, @@ -29,7 +33,9 @@ CoevaluationForDualWithGivenTensorProduct := rec( MorphismFromBidual := rec( filter_list := [ "category", "object" ], - io_type := [ [ "a" ], [ "s", "a" ] ], + input_arguments_names := [ "cat", "a" ], + output_range_getter_string := "a", + output_range_getter_preconditions := [ ], output_source_getter_string := "DualOnObjects( cat, DualOnObjects( cat, a ) )", output_source_getter_preconditions := [ [ "DualOnObjects", 2 ] ], output_range_getter_string := "a", @@ -41,7 +47,11 @@ MorphismFromBidual := rec( MorphismFromBidualWithGivenBidual := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "a", "s" ], [ "s", "a" ] ], + input_arguments_names := [ "cat", "a", "s" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "a", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "MorphismToCoBidualWithGivenCoBidual", dual_arguments_reversed := false, @@ -77,7 +87,7 @@ TensorProductInternalHomCompatibilityMorphismInverseWithGivenObjects := rec( MorphismFromInternalHomToTensorProduct := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "a", "b" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "a", "b" ], output_source_getter_string := "InternalHomOnObjects( cat, a, b )", output_source_getter_preconditions := [ [ "InternalHomOnObjects", 1 ] ], output_range_getter_string := "TensorProductOnObjects( cat, DualOnObjects( cat, a ), b )", @@ -91,7 +101,11 @@ MorphismFromInternalHomToTensorProduct := rec( MorphismFromInternalHomToTensorProductWithGivenObjects := rec( filter_list := [ "category", "object", "object", "object", "object" ], - io_type := [ [ "s", "a", "b", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "a", "b", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "MorphismFromTensorProductToInternalCoHomWithGivenObjects", dual_with_given_objects_reversed := true, @@ -99,7 +113,7 @@ MorphismFromInternalHomToTensorProductWithGivenObjects := rec( TraceMap := rec( filter_list := [ "category", "morphism" ], - io_type := [ [ "alpha" ], [ "u", "u" ] ], + input_arguments_names := [ "cat", "alpha" ], return_type := "morphism", dual_operation := "CoTraceMap", # Test in RigidSymmetricClosedMonoidalCategoriesTest @@ -107,7 +121,7 @@ TraceMap := rec( RankMorphism := rec( filter_list := [ "category", "object" ], - io_type := [ [ "a" ], [ "u", "u" ] ], + input_arguments_names := [ "cat", "a" ], return_type := "morphism", dual_operation := "CoRankMorphism", # Test in RigidSymmetricClosedMonoidalCategoriesTest @@ -115,7 +129,7 @@ RankMorphism := rec( IsomorphismFromTensorProductWithDualObjectToInternalHom := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "a", "b" ], [ "t", "i" ] ], + input_arguments_names := [ "cat", "a", "b" ], return_type := "morphism", dual_operation := "IsomorphismFromInternalCoHomToTensorProductWithCoDualObject", dual_arguments_reversed := true, @@ -124,7 +138,7 @@ IsomorphismFromTensorProductWithDualObjectToInternalHom := rec( IsomorphismFromInternalHomToTensorProductWithDualObject := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "a", "b" ], [ "i", "t" ] ], + input_arguments_names := [ "cat", "a", "b" ], return_type := "morphism", dual_operation := "IsomorphismFromTensorProductWithCoDualObjectToInternalCoHom", dual_arguments_reversed := false, diff --git a/MonoidalCategories/gap/RigidSymmetricCoclosedMonoidalCategoriesMethodRecord.gi b/MonoidalCategories/gap/RigidSymmetricCoclosedMonoidalCategoriesMethodRecord.gi index d42b8b7568..f2ce43cb58 100644 --- a/MonoidalCategories/gap/RigidSymmetricCoclosedMonoidalCategoriesMethodRecord.gi +++ b/MonoidalCategories/gap/RigidSymmetricCoclosedMonoidalCategoriesMethodRecord.gi @@ -8,7 +8,7 @@ InstallValue( RIGID_SYMMETRIC_COCLOSED_MONOIDAL_CATEGORIES_METHOD_NAME_RECORD, r CoclosedCoevaluationForCoDual := rec( filter_list := [ "category", "object" ], - io_type := [ [ "a" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "a" ], output_source_getter_string := "TensorProductOnObjects( cat, a, CoDualOnObjects( cat, a ) )", output_source_getter_preconditions := [ [ "TensorProductOnObjects", 1 ], [ "CoDualOnObjects", 1 ] ], output_range_getter_string := "TensorUnit( cat )", @@ -21,7 +21,11 @@ CoclosedCoevaluationForCoDual := rec( CoclosedCoevaluationForCoDualWithGivenTensorProduct := rec( filter_list := [ "category", "object", "object", "object" ], - io_type := [ [ "s", "a", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "a", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "CoevaluationForDualWithGivenTensorProduct", dual_arguments_reversed := true, @@ -29,7 +33,9 @@ CoclosedCoevaluationForCoDualWithGivenTensorProduct := rec( MorphismToCoBidual := rec( filter_list := [ "category", "object" ], - io_type := [ [ "a" ], [ "a", "r" ] ], + input_arguments_names := [ "cat", "a" ], + output_source_getter_string := "a", + output_source_getter_preconditions := [ ], output_source_getter_string := "a", output_range_getter_string := "CoDualOnObjects( cat, CoDualOnObjects( cat, a ) )", output_range_getter_preconditions := [ [ "CoDualOnObjects", 2 ] ], @@ -41,7 +47,11 @@ MorphismToCoBidual := rec( MorphismToCoBidualWithGivenCoBidual := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "a", "r" ], [ "a", "r" ] ], + input_arguments_names := [ "cat", "a", "r" ], + output_source_getter_string := "a", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "MorphismFromBidualWithGivenBidual", dual_arguments_reversed := false, @@ -77,7 +87,7 @@ InternalCoHomTensorProductCompatibilityMorphismInverseWithGivenObjects := rec( MorphismFromTensorProductToInternalCoHom := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "a", "b" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "a", "b" ], output_source_getter_string := "TensorProductOnObjects( cat, CoDualOnObjects( cat, a ), b )", output_source_getter_preconditions := [ [ "TensorProductOnObjects", 1 ], [ "CoDualOnObjects", 1 ] ], output_range_getter_string := "InternalCoHomOnObjects( cat, b, a )", @@ -91,7 +101,11 @@ MorphismFromTensorProductToInternalCoHom := rec( MorphismFromTensorProductToInternalCoHomWithGivenObjects := rec( filter_list := [ "category", "object", "object", "object", "object" ], - io_type := [ [ "s", "a", "b", "r" ], [ "s", "r" ] ], + input_arguments_names := [ "cat", "s", "a", "b", "r" ], + output_source_getter_string := "s", + output_source_getter_preconditions := [ ], + output_range_getter_string := "r", + output_range_getter_preconditions := [ ], return_type := "morphism", dual_operation := "MorphismFromInternalHomToTensorProductWithGivenObjects", dual_with_given_objects_reversed := true, @@ -99,7 +113,7 @@ MorphismFromTensorProductToInternalCoHomWithGivenObjects := rec( CoTraceMap := rec( filter_list := [ "category", "morphism" ], - io_type := [ [ "alpha" ], [ "u", "u" ] ], + input_arguments_names := [ "cat", "alpha" ], return_type := "morphism", dual_operation := "TraceMap", # Test in RigidSymmetricCoclosedMonoidalCategoriesTest @@ -107,7 +121,7 @@ CoTraceMap := rec( CoRankMorphism := rec( filter_list := [ "category", "object" ], - io_type := [ [ "a" ], [ "u", "u" ] ], + input_arguments_names := [ "cat", "a" ], return_type := "morphism", dual_operation := "RankMorphism", # Test in RigidSymmetricCoclosedMonoidalCategoriesTest @@ -115,7 +129,7 @@ CoRankMorphism := rec( IsomorphismFromInternalCoHomToTensorProductWithCoDualObject := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "a", "b" ], [ "i", "t" ] ], + input_arguments_names := [ "cat", "a", "b" ], return_type := "morphism", dual_operation := "IsomorphismFromTensorProductWithDualObjectToInternalHom", dual_arguments_reversed := true, @@ -124,7 +138,7 @@ IsomorphismFromInternalCoHomToTensorProductWithCoDualObject := rec( IsomorphismFromTensorProductWithCoDualObjectToInternalCoHom := rec( filter_list := [ "category", "object", "object" ], - io_type := [ [ "a", "b" ], [ "t", "i" ] ], + input_arguments_names := [ "cat", "a", "b" ], return_type := "morphism", dual_operation := "IsomorphismFromInternalHomToTensorProductWithDualObject", dual_arguments_reversed := false,