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 7d66849 commit 7e81796
Show file tree
Hide file tree
Showing 4 changed files with 16 additions and 16 deletions.
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
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
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
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 7e81796

Please sign in to comment.