Skip to content

Commit

Permalink
WithGiven* for MorphismFromInternalHomToTensorProductWithGivenObjects
Browse files Browse the repository at this point in the history
  • Loading branch information
Tom Kuhmichel committed Oct 17, 2023
1 parent 8e42dae commit 323d31f
Showing 1 changed file with 12 additions and 12 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -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 );

Expand Down

0 comments on commit 323d31f

Please sign in to comment.