Skip to content

Commit

Permalink
WithGiven* in derivations of *Compose
Browse files Browse the repository at this point in the history
  • Loading branch information
Tom Kuhmichel committed Oct 17, 2023
1 parent 174604f commit c1b9f7f
Show file tree
Hide file tree
Showing 5 changed files with 22 additions and 16 deletions.
6 changes: 6 additions & 0 deletions CartesianCategories/gap/CartesianClosedCategoriesMethodRecord.gi
View file
Original file line number Diff line number Diff line change
Expand Up @@ -29,6 +29,7 @@ ExponentialOnMorphisms := rec(
return_type := "morphism",
dual_operation := "CoexponentialOnMorphisms",
dual_arguments_reversed := true,
compatible_with_congruence_of_morphisms := true,
# Test in CartesianClosedCategoriesTest
),

Expand All @@ -42,6 +43,7 @@ ExponentialOnMorphismsWithGivenExponentials := rec(
return_type := "morphism",
dual_operation := "CoexponentialOnMorphismsWithGivenCoexponentials",
dual_arguments_reversed := true,
compatible_with_congruence_of_morphisms := true,
),

CartesianEvaluationMorphism := rec(
Expand Down Expand Up @@ -107,6 +109,7 @@ DirectProductToExponentialAdjunctionMap := rec(
return_type := "morphism",
dual_operation := "CoproductToCoexponentialAdjunctionMap",
dual_arguments_reversed := false,
compatible_with_congruence_of_morphisms := true,
# Test in CartesianClosedCategoriesTest
),

Expand All @@ -131,6 +134,7 @@ ExponentialToDirectProductAdjunctionMap := rec(
dual_operation := "CoexponentialToCoproductAdjunctionMap",
dual_preprocessor_func := { cat, a, b, g } -> NTuple( 4, Opposite( cat ), Opposite( b ), Opposite( a ), Opposite( g ) ),
dual_arguments_reversed := false,
compatible_with_congruence_of_morphisms := true,
# Test in CartesianClosedCategoriesTest
),

Expand Down Expand Up @@ -217,6 +221,7 @@ CartesianDualOnMorphisms := rec(
with_given_object_position := "both",
return_type := "morphism",
dual_operation := "CocartesianDualOnMorphisms",
compatible_with_congruence_of_morphisms := true,
# Test in CartesianClosedCategoriesTest
),

Expand All @@ -230,6 +235,7 @@ CartesianDualOnMorphismsWithGivenCartesianDuals := rec(
return_type := "morphism",
dual_operation := "CocartesianDualOnMorphismsWithGivenCocartesianDuals",
dual_arguments_reversed := true,
compatible_with_congruence_of_morphisms := true,
),

CartesianEvaluationForCartesianDual := rec(
Expand Down
8 changes: 4 additions & 4 deletions CartesianCategories/gap/SymmetricCartesianClosedCategoriesDerivedMethods.gi
View file
Original file line number Diff line number Diff line change
Expand Up @@ -861,7 +861,7 @@ AddDerivationToCAP( CartesianPostComposeMorphismWithGivenObjects,
"CartesianPostComposeMorphismWithGivenObjects using CartesianPreComposeMorphism and braiding",
[ [ CartesianBraiding, 1 ],
[ ExponentialOnObjects, 2 ],
[ PreCompose, 1 ],
[ PreComposeList, 1 ],
[ CartesianPreComposeMorphism, 1 ] ],

function( cat, source, a, b, c, range )
Expand All @@ -879,7 +879,7 @@ AddDerivationToCAP( CartesianPostComposeMorphismWithGivenObjects,

braiding := CartesianBraiding( cat, ExponentialOnObjects( cat, b, c ), ExponentialOnObjects( cat, a, b ) );

return PreCompose( cat, braiding, CartesianPreComposeMorphism( cat, a, b, c ) );
return PreComposeList( cat, source, [ braiding, CartesianPreComposeMorphism( cat, a, b, c ) ], range );

end : CategoryFilter := IsCartesianClosedCategory );

Expand All @@ -888,7 +888,7 @@ AddDerivationToCAP( CartesianPreComposeMorphismWithGivenObjects,
"CartesianPreComposeMorphismWithGivenObjects using CartesianPostComposeMorphism and braiding",
[ [ CartesianBraiding, 1 ],
[ ExponentialOnObjects, 2 ],
[ PreCompose, 1 ],
[ PreComposeList, 1 ],
[ CartesianPostComposeMorphism, 1 ] ],

function( cat, source, a, b, c, range )
Expand All @@ -906,7 +906,7 @@ AddDerivationToCAP( CartesianPreComposeMorphismWithGivenObjects,

braiding := CartesianBraiding( cat, ExponentialOnObjects( cat, a, b ), ExponentialOnObjects( cat, b, c ) );

return PreCompose( cat, braiding, CartesianPostComposeMorphism( cat, a, b, c ) );
return PreComposeList( cat, source, [ braiding, CartesianPostComposeMorphism( cat, a, b, c ) ], range );

end : CategoryFilter := IsCartesianClosedCategory );

Expand Down
8 changes: 4 additions & 4 deletions CartesianCategories/gap/SymmetricCocartesianCoclosedCategoriesDerivedMethods.gi
View file
Original file line number Diff line number Diff line change
Expand Up @@ -869,7 +869,7 @@ AddDerivationToCAP( CocartesianPostCoComposeMorphismWithGivenObjects,
"CocartesianPostCoComposeMorphismWithGivenObjects using CocartesianPreCoComposeMorphism and braiding",
[ [ CocartesianBraiding, 1 ],
[ CoexponentialOnObjects, 2 ],
[ PreCompose, 1 ],
[ PreComposeList, 1 ],
[ CocartesianPreCoComposeMorphism, 1 ] ],

function( cat, source, a, b, c, range )
Expand All @@ -887,7 +887,7 @@ AddDerivationToCAP( CocartesianPostCoComposeMorphismWithGivenObjects,

braiding := CocartesianBraiding( cat, CoexponentialOnObjects( cat, b, c ), CoexponentialOnObjects( cat, a, b ) );

return PreCompose( cat, CocartesianPreCoComposeMorphism( cat, a, b, c ), braiding );
return PreComposeList( cat, source, [ CocartesianPreCoComposeMorphism( cat, a, b, c ), braiding ], range );

end : CategoryFilter := IsCocartesianCoclosedCategory );

Expand All @@ -896,7 +896,7 @@ AddDerivationToCAP( CocartesianPreCoComposeMorphismWithGivenObjects,
"CocartesianPreCoComposeMorphismWithGivenObjects using CocartesianPostCoComposeMorphism and braiding",
[ [ CocartesianBraiding, 1 ],
[ CoexponentialOnObjects, 2 ],
[ PreCompose, 1 ],
[ PreComposeList, 1 ],
[ CocartesianPostCoComposeMorphism, 1 ] ],

function( cat, source, a, b, c, range )
Expand All @@ -914,7 +914,7 @@ AddDerivationToCAP( CocartesianPreCoComposeMorphismWithGivenObjects,

braiding := CocartesianBraiding( cat, CoexponentialOnObjects( cat, a, b ), CoexponentialOnObjects( cat, b, c ) );

return PreCompose( cat, CocartesianPostCoComposeMorphism( cat, a, b, c ), braiding );
return PreComposeList( cat, source, [ CocartesianPostCoComposeMorphism( cat, a, b, c ), braiding ], range );

end : CategoryFilter := IsCocartesianCoclosedCategory );

Expand Down
8 changes: 4 additions & 4 deletions MonoidalCategories/gap/SymmetricClosedMonoidalCategoriesDerivedMethods.gi
View file
Original file line number Diff line number Diff line change
Expand Up @@ -858,7 +858,7 @@ AddDerivationToCAP( MonoidalPostComposeMorphismWithGivenObjects,
"MonoidalPostComposeMorphismWithGivenObjects using MonoidalPreComposeMorphism and braiding",
[ [ Braiding, 1 ],
[ InternalHomOnObjects, 2 ],
[ PreCompose, 1 ],
[ PreComposeList, 1 ],
[ MonoidalPreComposeMorphism, 1 ] ],

function( cat, source, a, b, c, range )
Expand All @@ -876,7 +876,7 @@ AddDerivationToCAP( MonoidalPostComposeMorphismWithGivenObjects,

braiding := Braiding( cat, InternalHomOnObjects( cat, b, c ), InternalHomOnObjects( cat, a, b ) );

return PreCompose( cat, braiding, MonoidalPreComposeMorphism( cat, a, b, c ) );
return PreComposeList( cat, source, [ braiding, MonoidalPreComposeMorphism( cat, a, b, c ) ], range );

end : CategoryFilter := IsSymmetricClosedMonoidalCategory );

Expand All @@ -885,7 +885,7 @@ AddDerivationToCAP( MonoidalPreComposeMorphismWithGivenObjects,
"MonoidalPreComposeMorphismWithGivenObjects using MonoidalPostComposeMorphism and braiding",
[ [ Braiding, 1 ],
[ InternalHomOnObjects, 2 ],
[ PreCompose, 1 ],
[ PreComposeList, 1 ],
[ MonoidalPostComposeMorphism, 1 ] ],

function( cat, source, a, b, c, range )
Expand All @@ -903,7 +903,7 @@ AddDerivationToCAP( MonoidalPreComposeMorphismWithGivenObjects,

braiding := Braiding( cat, InternalHomOnObjects( cat, a, b ), InternalHomOnObjects( cat, b, c ) );

return PreCompose( cat, braiding, MonoidalPostComposeMorphism( cat, a, b, c ) );
return PreComposeList( cat, source, [ braiding, MonoidalPostComposeMorphism( cat, a, b, c ) ], range );

end : CategoryFilter := IsSymmetricClosedMonoidalCategory );

Expand Down
8 changes: 4 additions & 4 deletions MonoidalCategories/gap/SymmetricCoclosedMonoidalCategoriesDerivedMethods.gi
View file
Original file line number Diff line number Diff line change
Expand Up @@ -866,7 +866,7 @@ AddDerivationToCAP( MonoidalPostCoComposeMorphismWithGivenObjects,
"MonoidalPostCoComposeMorphismWithGivenObjects using MonoidalPreCoComposeMorphism and braiding",
[ [ Braiding, 1 ],
[ InternalCoHomOnObjects, 2 ],
[ PreCompose, 1 ],
[ PreComposeList, 1 ],
[ MonoidalPreCoComposeMorphism, 1 ] ],

function( cat, source, a, b, c, range )
Expand All @@ -884,7 +884,7 @@ AddDerivationToCAP( MonoidalPostCoComposeMorphismWithGivenObjects,

braiding := Braiding( cat, InternalCoHomOnObjects( cat, b, c ), InternalCoHomOnObjects( cat, a, b ) );

return PreCompose( cat, MonoidalPreCoComposeMorphism( cat, a, b, c ), braiding );
return PreComposeList( cat, source, [ MonoidalPreCoComposeMorphism( cat, a, b, c ), braiding ], range );

end : CategoryFilter := IsSymmetricCoclosedMonoidalCategory );

Expand All @@ -893,7 +893,7 @@ AddDerivationToCAP( MonoidalPreCoComposeMorphismWithGivenObjects,
"MonoidalPreCoComposeMorphismWithGivenObjects using MonoidalPostCoComposeMorphism and braiding",
[ [ Braiding, 1 ],
[ InternalCoHomOnObjects, 2 ],
[ PreCompose, 1 ],
[ PreComposeList, 1 ],
[ MonoidalPostCoComposeMorphism, 1 ] ],

function( cat, source, a, b, c, range )
Expand All @@ -911,7 +911,7 @@ AddDerivationToCAP( MonoidalPreCoComposeMorphismWithGivenObjects,

braiding := Braiding( cat, InternalCoHomOnObjects( cat, a, b ), InternalCoHomOnObjects( cat, b, c ) );

return PreCompose( cat, MonoidalPostCoComposeMorphism( cat, a, b, c ), braiding );
return PreComposeList( cat, source, [ MonoidalPostCoComposeMorphism( cat, a, b, c ), braiding ], range );

end : CategoryFilter := IsSymmetricCoclosedMonoidalCategory );

Expand Down

0 comments on commit c1b9f7f

Please sign in to comment.