WithGiven* for monoidal Isomorphisms

CartesianCategories/gap/CartesianClosedCategoriesMethodRecord.gi

@@ -29,7 +29,6 @@ ExponentialOnMorphisms := rec(
   return_type := "morphism",
   dual_operation := "CoexponentialOnMorphisms",
   dual_arguments_reversed := true,
-  compatible_with_congruence_of_morphisms := true,
   # Test in CartesianClosedCategoriesTest
 ),
 
@@ -43,7 +42,6 @@ ExponentialOnMorphismsWithGivenExponentials := rec(
   return_type := "morphism",
   dual_operation := "CoexponentialOnMorphismsWithGivenCoexponentials",
   dual_arguments_reversed := true,
-  compatible_with_congruence_of_morphisms := true,
 ),
 
 CartesianEvaluationMorphism := rec(
@@ -109,7 +107,6 @@ DirectProductToExponentialAdjunctionMap := rec(
   return_type := "morphism",
   dual_operation := "CoproductToCoexponentialAdjunctionMap",
   dual_arguments_reversed := false,
-  compatible_with_congruence_of_morphisms := true,
   # Test in CartesianClosedCategoriesTest
 ),
 
@@ -134,7 +131,6 @@ 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
 ),
 
@@ -221,7 +217,6 @@ CartesianDualOnMorphisms := rec(
   with_given_object_position := "both",
   return_type := "morphism",
   dual_operation := "CocartesianDualOnMorphisms",
-  compatible_with_congruence_of_morphisms := true,
   # Test in CartesianClosedCategoriesTest
 ),
 
@@ -235,7 +230,6 @@ CartesianDualOnMorphismsWithGivenCartesianDuals := rec(
   return_type := "morphism",
   dual_operation := "CocartesianDualOnMorphismsWithGivenCocartesianDuals",
   dual_arguments_reversed := true,
-  compatible_with_congruence_of_morphisms := true,
 ),
 
 CartesianEvaluationForCartesianDual := rec(

CartesianCategories/gap/SymmetricCartesianClosedCategoriesDerivedMethods.gi

@@ -534,7 +534,7 @@ end : CategoryFilter := IsCartesianClosedCategory );
 AddDerivationToCAP( IsomorphismFromObjectToExponentialWithGivenExponential,
                     "IsomorphismFromObjectToExponentialWithGivenExponential using the coevaluation morphism",
                     [ [ TerminalObject, 1 ],
-                      [ PreCompose, 1 ],
+                      [ PreComposeList, 1 ],
                       [ CartesianCoevaluationMorphism, 1 ],
                       [ ExponentialOnMorphisms, 1 ],
                       [ IdentityMorphism, 1 ],
@@ -555,19 +555,19 @@ AddDerivationToCAP( IsomorphismFromObjectToExponentialWithGivenExponential,
 
     unit := TerminalObject( cat );
 
-    return PreCompose( cat,
-             CartesianCoevaluationMorphism( cat, a, unit ),
-             ExponentialOnMorphisms( cat,
-               IdentityMorphism( cat, unit ),
-               CartesianRightUnitor( cat, a ) ) );
+    return PreComposeList( cat,
+                a,
+                [ CartesianCoevaluationMorphism( cat, a, unit ),
+                  ExponentialOnMorphisms( cat, IdentityMorphism( cat, unit ), CartesianRightUnitor( cat, a ) ) ],
+                internal_hom );
 
 end : CategoryFilter := IsCartesianClosedCategory );
 
 ##
 AddDerivationToCAP( IsomorphismFromObjectToExponentialWithGivenExponential,
                     "IsomorphismFromObjectToExponentialWithGivenExponential as the adjoint of the right unitor",
                     [ [ TerminalObject, 1 ],
-                      [ DirectProductToExponentialAdjunctionMap, 1 ],
+                      [ DirectProductToExponentialAdjunctionMapWithGivenExponential, 1 ],
                       [ CartesianRightUnitor, 1 ] ],
 
   function( cat, a, internal_hom )
@@ -576,10 +576,11 @@ AddDerivationToCAP( IsomorphismFromObjectToExponentialWithGivenExponential,
     #
     # Adjoint( ρ_a ) = ( a → Exp(1,a) )
 
-    return DirectProductToExponentialAdjunctionMap( cat,
+    return DirectProductToExponentialAdjunctionMapWithGivenExponential( cat,
                    a,
                    TerminalObject( cat ),
-                   CartesianRightUnitor( cat, a ) );
+                   CartesianRightUnitor( cat, a ),
+                   internal_hom );
 
 end : CategoryFilter := IsCartesianClosedCategory );
 
@@ -600,7 +601,7 @@ end : CategoryFilter := IsCartesianClosedCategory );
 AddDerivationToCAP( IsomorphismFromExponentialToObjectWithGivenExponential,
                     "IsomorphismFromExponentialToObjectWithGivenExponential using the evaluation morphism",
                     [ [ TerminalObject, 1 ],
-                      [ PreCompose, 1 ],
+                      [ PreComposeList, 1 ],
                       [ CartesianRightUnitorInverse, 1 ],
                       [ CartesianEvaluationMorphism, 1 ] ],
 
@@ -616,9 +617,11 @@ AddDerivationToCAP( IsomorphismFromExponentialToObjectWithGivenExponential,
     #      v
     #      a
 
-    return PreCompose( cat,
-                   CartesianRightUnitorInverse( cat, internal_hom ),
-                   CartesianEvaluationMorphism( cat, TerminalObject( cat ), a ) );
+    return PreComposeList( cat,
+                internal_hom,
+                [ CartesianRightUnitorInverse( cat, internal_hom ),
+                  CartesianEvaluationMorphism( cat, TerminalObject( cat ), a ) ],
+                a );
 
 end : CategoryFilter := IsCartesianClosedCategory );
 

CartesianCategories/gap/SymmetricCocartesianCoclosedCategoriesDerivedMethods.gi

@@ -542,7 +542,7 @@ end : CategoryFilter := IsCocartesianCoclosedCategory );
 AddDerivationToCAP( IsomorphismFromCoexponentialToObjectWithGivenCoexponential,
                     "IsomorphismFromCoexponentialToObjectWithGivenCoexponential using the cocartesian coevaluation morphism",
                     [ [ InitialObject, 1 ],
-                      [ PreCompose, 1 ],
+                      [ PreComposeList, 1 ],
                       [ CoexponentialOnMorphisms, 1 ],
                       [ CocartesianRightUnitorInverse, 1 ],
                       [ IdentityMorphism, 1 ],
@@ -563,20 +563,21 @@ AddDerivationToCAP( IsomorphismFromCoexponentialToObjectWithGivenCoexponential,
 
     unit := InitialObject( cat );
 
-    return PreCompose( cat,
-                   CoexponentialOnMorphisms( cat,
-                           CocartesianRightUnitorInverse( cat, a ),
-                           IdentityMorphism( cat, unit ) ),
-
-                   CocartesianCoevaluationMorphism( cat, a, unit ) );
+    return PreComposeList( cat,
+                internal_cohom,
+                [ CoexponentialOnMorphisms( cat,
+                        CocartesianRightUnitorInverse( cat, a ),
+                        IdentityMorphism( cat, unit ) ),
+                  CocartesianCoevaluationMorphism( cat, a, unit ) ],
+                a );
 
 end : CategoryFilter := IsCocartesianCoclosedCategory );
 
 ##
 AddDerivationToCAP( IsomorphismFromCoexponentialToObjectWithGivenCoexponential,
                     "IsomorphismFromCoexponentialToObjectWithGivenCoexponential as the adjoint of the right inverse unitor",
                     [ [ InitialObject, 1 ],
-                      [ CoproductToCoexponentialAdjunctionMap, 1 ],
+                      [ CoproductToCoexponentialAdjunctionMapWithGivenCoexponential, 1 ],
                       [ CocartesianRightUnitorInverse, 1 ] ],
 
   function( cat, a, internal_cohom )
@@ -585,10 +586,11 @@ AddDerivationToCAP( IsomorphismFromCoexponentialToObjectWithGivenCoexponential,
     #
     # Adjoint( (ρ_a)^-1 ) = ( Coexp(a,1) → a )
 
-    return CoproductToCoexponentialAdjunctionMap( cat,
+    return CoproductToCoexponentialAdjunctionMapWithGivenCoexponential( cat,
                    a,
                    InitialObject( cat ),
-                   CocartesianRightUnitorInverse( cat, a ) );
+                   CocartesianRightUnitorInverse( cat, a ),
+                   internal_cohom );
 
 end : CategoryFilter := IsCocartesianCoclosedCategory );
 
@@ -609,7 +611,7 @@ end : CategoryFilter := IsCocartesianCoclosedCategory );
 AddDerivationToCAP( IsomorphismFromObjectToCoexponentialWithGivenCoexponential,
                     "IsomorphismFromObjectToCoexponentialWithGivenCoexponential using the cocartesian evaluation morphism",
                     [ [ InitialObject, 1 ],
-                      [ PreCompose, 1 ],
+                      [ PreComposeList, 1 ],
                       [ CocartesianEvaluationMorphism, 1 ],
                       [ CocartesianRightUnitor, 1 ] ],
 
@@ -625,9 +627,11 @@ AddDerivationToCAP( IsomorphismFromObjectToCoexponentialWithGivenCoexponential,
     #       v
     #   Coexp(a,1)
 
-    return PreCompose( cat,
-                   CocartesianEvaluationMorphism( cat, a, InitialObject( cat ) ),
-                   CocartesianRightUnitor( cat, internal_cohom ) );
+    return PreComposeList( cat,
+                   a,
+                   [ CocartesianEvaluationMorphism( cat, a, InitialObject( cat ) ),
+                     CocartesianRightUnitor( cat, internal_cohom ) ],
+                   internal_cohom );
 
 end : CategoryFilter := IsCocartesianCoclosedCategory );