From 323d31fe95746864d9b3a62d39874caebb9c508c Mon Sep 17 00:00:00 2001 From: Tom Kuhmichel Date: Mon, 9 Oct 2023 13:30:42 +0200 Subject: [PATCH] WithGiven* for MorphismFromInternalHomToTensorProductWithGivenObjects --- ...cClosedMonoidalCategoriesDerivedMethods.gi | 24 +++++++++---------- 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/MonoidalCategories/gap/RigidSymmetricClosedMonoidalCategoriesDerivedMethods.gi b/MonoidalCategories/gap/RigidSymmetricClosedMonoidalCategoriesDerivedMethods.gi index b84281b18b..69751f412f 100644 --- a/MonoidalCategories/gap/RigidSymmetricClosedMonoidalCategoriesDerivedMethods.gi +++ b/MonoidalCategories/gap/RigidSymmetricClosedMonoidalCategoriesDerivedMethods.gi @@ -416,18 +416,18 @@ AddDerivationToCAP( MorphismFromInternalHomToTensorProductWithGivenObjects, unit := TensorUnit( cat ); - return PostComposeList( cat, [ - TensorProductOnMorphisms( cat, - IsomorphismFromInternalHomIntoTensorUnitToDualObject( cat, a ), - IsomorphismFromInternalHomToObject( cat, b ) ), - - TensorProductInternalHomCompatibilityMorphismInverse( cat, - [ a, unit, unit, b ] ), - - InternalHomOnMorphisms( cat, - RightUnitor( cat, a ), - LeftUnitorInverse( cat, b ) ), - ] ); + return PostComposeList( cat, + internal_hom, + [ TensorProductOnMorphisms( cat, + IsomorphismFromInternalHomIntoTensorUnitToDualObject( cat, a ), + IsomorphismFromInternalHomToObject( cat, b ) ), + + TensorProductInternalHomCompatibilityMorphismInverse( cat, [ a, unit, unit, b ] ), + + InternalHomOnMorphisms( cat, + RightUnitor( cat, a ), + LeftUnitorInverse( cat, b ) ) ], + tensor_object ); end : CategoryFilter := IsRigidSymmetricClosedMonoidalCategory );