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 Nov 29, 2023
1 parent d8e4c21 commit d962219
Show file tree
Hide file tree
Showing 5 changed files with 210 additions and 194 deletions.
30 changes: 20 additions & 10 deletions CartesianCategories/gap/SymmetricCartesianClosedCategoriesDerivedMethods.gi
View file
Original file line number Diff line number Diff line change
Expand Up @@ -859,13 +859,14 @@ end : CategoryFilter := IsCartesianClosedCategory );
##
AddDerivationToCAP( CartesianPostComposeMorphismWithGivenObjects,
"CartesianPostComposeMorphismWithGivenObjects using CartesianPreComposeMorphism and braiding",
[ [ CartesianBraiding, 1 ],
[ [ CartesianBraidingWithGivenDirectProducts, 1 ],
[ ExponentialOnObjects, 2 ],
[ PreCompose, 1 ],
[ CartesianPreComposeMorphism, 1 ] ],
[ DirectProduct, 1],
[ CartesianPreComposeMorphismWithGivenObjects, 1 ] ],

function( cat, source, a, b, c, range )
local braiding;
local exp_ab, exp_bc, exp_ab_x_exp_bc, braiding;

# Exp(b,c) × Exp(a,b)
# |
Expand All @@ -877,22 +878,27 @@ AddDerivationToCAP( CartesianPostComposeMorphismWithGivenObjects,
# v
# Exp(a,c)

braiding := CartesianBraiding( cat, ExponentialOnObjects( cat, b, c ), ExponentialOnObjects( cat, a, b ) );
exp_ab := ExponentialOnObjects( cat, a, b );
exp_bc := ExponentialOnObjects( cat, b, c );
exp_ab_x_exp_bc := BinaryDirectProduct( cat, exp_ab, exp_bc );

braiding := CartesianBraidingWithGivenDirectProducts( cat, source, exp_bc, exp_ab, exp_ab_x_exp_bc );

return PreCompose( cat, braiding, CartesianPreComposeMorphism( cat, a, b, c ) );
return PreCompose( cat, braiding, CartesianPreComposeMorphismWithGivenObjects( cat, exp_ab_x_exp_bc, a, b, c, range ) );

end : CategoryFilter := IsCartesianClosedCategory );

##
AddDerivationToCAP( CartesianPreComposeMorphismWithGivenObjects,
"CartesianPreComposeMorphismWithGivenObjects using CartesianPostComposeMorphism and braiding",
[ [ CartesianBraiding, 1 ],
[ [ CartesianBraidingWithGivenDirectProducts, 1 ],
[ ExponentialOnObjects, 2 ],
[ PreCompose, 1 ],
[ CartesianPostComposeMorphism, 1 ] ],
[ DirectProduct, 1],
[ CartesianPostComposeMorphismWithGivenObjects, 1 ] ],

function( cat, source, a, b, c, range )
local braiding;
local exp_ab, exp_bc, exp_bc_x_exp_ab, braiding;

# Exp(a,b) × Exp(b,c)
# |
Expand All @@ -904,9 +910,13 @@ AddDerivationToCAP( CartesianPreComposeMorphismWithGivenObjects,
# v
# Exp(a,c)

braiding := CartesianBraiding( cat, ExponentialOnObjects( cat, a, b ), ExponentialOnObjects( cat, b, c ) );
exp_ab := ExponentialOnObjects( cat, a, b );
exp_bc := ExponentialOnObjects( cat, b, c );
exp_bc_x_exp_ab := BinaryDirectProduct( cat, exp_bc, exp_ab );

braiding := CartesianBraidingWithGivenDirectProducts( cat, source, exp_bc, exp_ab, exp_bc_x_exp_ab );

return PreCompose( cat, braiding, CartesianPostComposeMorphism( cat, a, b, c ) );
return PreCompose( cat, braiding, CartesianPostComposeMorphismWithGivenObjects( cat, exp_bc_x_exp_ab, a, b, c, range ) );

end : CategoryFilter := IsCartesianClosedCategory );

Expand Down
32 changes: 21 additions & 11 deletions CartesianCategories/gap/SymmetricCocartesianCoclosedCategoriesDerivedMethods.gi
View file
Original file line number Diff line number Diff line change
Expand Up @@ -867,13 +867,14 @@ end : CategoryFilter := IsCocartesianCoclosedCategory );
##
AddDerivationToCAP( CocartesianPostCoComposeMorphismWithGivenObjects,
"CocartesianPostCoComposeMorphismWithGivenObjects using CocartesianPreCoComposeMorphism and braiding",
[ [ CocartesianBraiding, 1 ],
[ [ CocartesianBraidingWithGivenCoproducts, 1 ],
[ CoexponentialOnObjects, 2 ],
[ PreCompose, 1 ],
[ CocartesianPreCoComposeMorphism, 1 ] ],
[ Coproduct, 1 ],
[ CocartesianPreCoComposeMorphismWithGivenObjects, 1 ] ],

function( cat, source, a, b, c, range )
local braiding;
local coexp_ab, coexp_bc, coexp_bc_x_coexp_ab, braiding;

# Coexp(a,c)
# |
Expand All @@ -885,22 +886,27 @@ AddDerivationToCAP( CocartesianPostCoComposeMorphismWithGivenObjects,
# v
# Coexp(a,b) ⊔ Coexp(b,c)

braiding := CocartesianBraiding( cat, CoexponentialOnObjects( cat, b, c ), CoexponentialOnObjects( cat, a, b ) );
coexp_ab := CoexponentialOnObjects( cat, a, b );
coexp_bc := CoexponentialOnObjects( cat, b, c );
coexp_bc_x_coexp_ab := BinaryCoproduct( cat, coexp_bc, coexp_ab );

braiding := CocartesianBraidingWithGivenCoproducts( cat, coexp_bc_x_coexp_ab, coexp_bc, coexp_ab, range );

return PreCompose( cat, CocartesianPreCoComposeMorphism( cat, a, b, c ), braiding );
return PreCompose( cat, CocartesianPreCoComposeMorphismWithGivenObjects( cat, source, a, b, c, coexp_bc_x_coexp_ab ), braiding );

end : CategoryFilter := IsCocartesianCoclosedCategory );

##
AddDerivationToCAP( CocartesianPreCoComposeMorphismWithGivenObjects,
"CocartesianPreCoComposeMorphismWithGivenObjects using CocartesianPostCoComposeMorphism and braiding",
[ [ CocartesianBraiding, 1 ],
[ [ CocartesianBraidingWithGivenCoproducts, 1 ],
[ CoexponentialOnObjects, 2 ],
[ PreCompose, 1 ],
[ CocartesianPostCoComposeMorphism, 1 ] ],
[ Coproduct, 1 ],
[ CocartesianPostCoComposeMorphismWithGivenObjects, 1 ] ],

function( cat, source, a, b, c, range )
local braiding;
local coexp_ab, coexp_bc, coexp_ab_x_coexp_bc, braiding;

# Coexp(a,c)
# |
Expand All @@ -911,10 +917,14 @@ AddDerivationToCAP( CocartesianPreCoComposeMorphismWithGivenObjects,
# | B_( Coexp(a,b), Coexp(b,c) )
# v
# Coexp(b,c) ⊔ Coexp(a,b)

braiding := CocartesianBraiding( cat, CoexponentialOnObjects( cat, a, b ), CoexponentialOnObjects( cat, b, c ) );

return PreCompose( cat, CocartesianPostCoComposeMorphism( cat, a, b, c ), braiding );
coexp_ab := CoexponentialOnObjects( cat, a, b );
coexp_bc := CoexponentialOnObjects( cat, b, c );
coexp_ab_x_coexp_bc := BinaryCoproduct( cat, coexp_ab, coexp_bc );

braiding := CocartesianBraidingWithGivenCoproducts( cat, coexp_ab_x_coexp_bc, coexp_ab, coexp_bc, range );

return PreCompose( cat, CocartesianPostCoComposeMorphismWithGivenObjects( cat, source, a, b, c, coexp_ab_x_coexp_bc ), braiding );

end : CategoryFilter := IsCocartesianCoclosedCategory );

Expand Down
Loading

0 comments on commit d962219

Please sign in to comment.