Closed zickgraf closed 9 months ago
Yes, this is just a special case of the adjunction of the closed monoidal structure, no symmetric monoidal structure is needed.
@mohamed-barakat The derivation mentioned in the first comment seems to not be touched by #1561, so I guess this is not (fully) fixed?
EvaluationMorphism is derived as the counit of the tensor-hom adjunction: https://github.com/homalg-project/CAP_project/blob/39f43d3fb99140ece7a745f702289e7b9a71d1c1/MonoidalCategories/gap/SymmetricClosedMonoidalCategoriesDerivedMethods.gi#L637-L651
This derivation only triggers for
IsSymmetricClosedMonoidalCategory
, not forIsClosedMonoidalCategory
. I think this is for historic reasons: This derivation already existed before 57d73bb20092f722049eaafc4e1e3bcc133f2809 and before this commit there was noIsClosedMonoidalCategory
. So I think the filter could be relaxed toIsClosedMonoidalCategory
.@mohamed-barakat @sebastianpos Is this correct or am I missing something?