Skip to content

Commit

Permalink
WithGiven* for monoidal Isomorphisms
Browse files Browse the repository at this point in the history
  • Loading branch information
Tom Kuhmichel committed Oct 17, 2023
1 parent 7e81796 commit 8e42dae
Show file tree
Hide file tree
Showing 5 changed files with 136 additions and 126 deletions.
29 changes: 16 additions & 13 deletions CartesianCategories/gap/SymmetricCartesianClosedCategoriesDerivedMethods.gi
View file
Original file line number Diff line number Diff line change
Expand Up @@ -534,7 +534,7 @@ end : CategoryFilter := IsCartesianClosedCategory );
AddDerivationToCAP( IsomorphismFromObjectToExponentialWithGivenExponential,
"IsomorphismFromObjectToExponentialWithGivenExponential using the coevaluation morphism",
[ [ TerminalObject, 1 ],
[ PreCompose, 1 ],
[ PreComposeList, 1 ],
[ CartesianCoevaluationMorphism, 1 ],
[ ExponentialOnMorphisms, 1 ],
[ IdentityMorphism, 1 ],
Expand All @@ -555,19 +555,19 @@ AddDerivationToCAP( IsomorphismFromObjectToExponentialWithGivenExponential,

unit := TerminalObject( cat );

return PreCompose( cat,
CartesianCoevaluationMorphism( cat, a, unit ),
ExponentialOnMorphisms( cat,
IdentityMorphism( cat, unit ),
CartesianRightUnitor( cat, a ) ) );
return PreComposeList( cat,
a,
[ CartesianCoevaluationMorphism( cat, a, unit ),
ExponentialOnMorphisms( cat, IdentityMorphism( cat, unit ), CartesianRightUnitor( cat, a ) ) ],
internal_hom );

end : CategoryFilter := IsCartesianClosedCategory );

##
AddDerivationToCAP( IsomorphismFromObjectToExponentialWithGivenExponential,
"IsomorphismFromObjectToExponentialWithGivenExponential as the adjoint of the right unitor",
[ [ TerminalObject, 1 ],
[ DirectProductToExponentialAdjunctionMap, 1 ],
[ DirectProductToExponentialAdjunctionMapWithGivenExponential, 1 ],
[ CartesianRightUnitor, 1 ] ],

function( cat, a, internal_hom )
Expand All @@ -576,10 +576,11 @@ AddDerivationToCAP( IsomorphismFromObjectToExponentialWithGivenExponential,
#
# Adjoint( ρ_a ) = ( a → Exp(1,a) )

return DirectProductToExponentialAdjunctionMap( cat,
return DirectProductToExponentialAdjunctionMapWithGivenExponential( cat,
a,
TerminalObject( cat ),
CartesianRightUnitor( cat, a ) );
CartesianRightUnitor( cat, a ),
internal_hom );

end : CategoryFilter := IsCartesianClosedCategory );

Expand All @@ -600,7 +601,7 @@ end : CategoryFilter := IsCartesianClosedCategory );
AddDerivationToCAP( IsomorphismFromExponentialToObjectWithGivenExponential,
"IsomorphismFromExponentialToObjectWithGivenExponential using the evaluation morphism",
[ [ TerminalObject, 1 ],
[ PreCompose, 1 ],
[ PreComposeList, 1 ],
[ CartesianRightUnitorInverse, 1 ],
[ CartesianEvaluationMorphism, 1 ] ],

Expand All @@ -616,9 +617,11 @@ AddDerivationToCAP( IsomorphismFromExponentialToObjectWithGivenExponential,
# v
# a

return PreCompose( cat,
CartesianRightUnitorInverse( cat, internal_hom ),
CartesianEvaluationMorphism( cat, TerminalObject( cat ), a ) );
return PreComposeList( cat,
internal_hom,
[ CartesianRightUnitorInverse( cat, internal_hom ),
CartesianEvaluationMorphism( cat, TerminalObject( cat ), a ) ],
a );

end : CategoryFilter := IsCartesianClosedCategory );

Expand Down
32 changes: 18 additions & 14 deletions CartesianCategories/gap/SymmetricCocartesianCoclosedCategoriesDerivedMethods.gi
View file
Original file line number Diff line number Diff line change
Expand Up @@ -542,7 +542,7 @@ end : CategoryFilter := IsCocartesianCoclosedCategory );
AddDerivationToCAP( IsomorphismFromCoexponentialToObjectWithGivenCoexponential,
"IsomorphismFromCoexponentialToObjectWithGivenCoexponential using the cocartesian coevaluation morphism",
[ [ InitialObject, 1 ],
[ PreCompose, 1 ],
[ PreComposeList, 1 ],
[ CoexponentialOnMorphisms, 1 ],
[ CocartesianRightUnitorInverse, 1 ],
[ IdentityMorphism, 1 ],
Expand All @@ -563,20 +563,21 @@ AddDerivationToCAP( IsomorphismFromCoexponentialToObjectWithGivenCoexponential,

unit := InitialObject( cat );

return PreCompose( cat,
CoexponentialOnMorphisms( cat,
CocartesianRightUnitorInverse( cat, a ),
IdentityMorphism( cat, unit ) ),

CocartesianCoevaluationMorphism( cat, a, unit ) );
return PreComposeList( cat,
internal_cohom,
[ CoexponentialOnMorphisms( cat,
CocartesianRightUnitorInverse( cat, a ),
IdentityMorphism( cat, unit ) ),
CocartesianCoevaluationMorphism( cat, a, unit ) ],
a );

end : CategoryFilter := IsCocartesianCoclosedCategory );

##
AddDerivationToCAP( IsomorphismFromCoexponentialToObjectWithGivenCoexponential,
"IsomorphismFromCoexponentialToObjectWithGivenCoexponential as the adjoint of the right inverse unitor",
[ [ InitialObject, 1 ],
[ CoproductToCoexponentialAdjunctionMap, 1 ],
[ CoproductToCoexponentialAdjunctionMapWithGivenCoexponential, 1 ],
[ CocartesianRightUnitorInverse, 1 ] ],

function( cat, a, internal_cohom )
Expand All @@ -585,10 +586,11 @@ AddDerivationToCAP( IsomorphismFromCoexponentialToObjectWithGivenCoexponential,
#
# Adjoint( (ρ_a)^-1 ) = ( Coexp(a,1) → a )

return CoproductToCoexponentialAdjunctionMap( cat,
return CoproductToCoexponentialAdjunctionMapWithGivenCoexponential( cat,
a,
InitialObject( cat ),
CocartesianRightUnitorInverse( cat, a ) );
CocartesianRightUnitorInverse( cat, a ),
internal_cohom );

end : CategoryFilter := IsCocartesianCoclosedCategory );

Expand All @@ -609,7 +611,7 @@ end : CategoryFilter := IsCocartesianCoclosedCategory );
AddDerivationToCAP( IsomorphismFromObjectToCoexponentialWithGivenCoexponential,
"IsomorphismFromObjectToCoexponentialWithGivenCoexponential using the cocartesian evaluation morphism",
[ [ InitialObject, 1 ],
[ PreCompose, 1 ],
[ PreComposeList, 1 ],
[ CocartesianEvaluationMorphism, 1 ],
[ CocartesianRightUnitor, 1 ] ],

Expand All @@ -625,9 +627,11 @@ AddDerivationToCAP( IsomorphismFromObjectToCoexponentialWithGivenCoexponential,
# v
# Coexp(a,1)

return PreCompose( cat,
CocartesianEvaluationMorphism( cat, a, InitialObject( cat ) ),
CocartesianRightUnitor( cat, internal_cohom ) );
return PreComposeList( cat,
a,
[ CocartesianEvaluationMorphism( cat, a, InitialObject( cat ) ),
CocartesianRightUnitor( cat, internal_cohom ) ],
internal_cohom );

end : CategoryFilter := IsCocartesianCoclosedCategory );

Expand Down
Loading

0 comments on commit 8e42dae

Please sign in to comment.