derived CartesianLeft/RightUnitorInverse and CocartesianLeft/RightUnitor

Author: mohamed-barakat

CartesianCategories/PackageInfo.g

@@ -10,7 +10,7 @@ SetPackageInfo( rec(
 
 PackageName := "CartesianCategories",
 Subtitle := "Cartesian and cocartesian categories and various subdoctrines",
-Version := "2026.06-03",
+Version := "2026.07-01",
 Date := ~.Version{[ 1 .. 10 ]},
 Date := (function ( ) if IsBound( GAPInfo.SystemEnvironment.GAP_PKG_RELEASE_DATE ) then return GAPInfo.SystemEnvironment.GAP_PKG_RELEASE_DATE; else return Concatenation( ~.Version{[ 1 .. 4 ]}, "-", ~.Version{[ 6, 7 ]}, "-01" ); fi; end)( ),
 License := "GPL-2.0-or-later",

CartesianCategories/examples/InfoStringOfInstalledOperationsOfCategory.g

@@ -13,7 +13,7 @@ distributive := DummyCategory( rec(
   properties := [ "IsBicartesianClosedCategory", "IsSkeletalCategory" ] ) );;
 
 InfoOfInstalledOperationsOfCategory( distributive );
-#! 21 primitive operations were used to derive 129 operations for this category \
+#! 21 primitive operations were used to derive 142 operations for this category \
 #! which algorithmically
 #! * IsBicartesianClosedCategory
 #! and not yet algorithmically

CartesianCategories/gap/CartesianCategoriesDerivedMethods_extra.gi

@@ -84,6 +84,70 @@ AddDerivationToCAP( CartesianRightUnitorWithGivenDirectProduct,
 
 end );
 
+##
+AddDerivationToCAP( CartesianLeftUnitorInverseWithGivenDirectProduct,
+                    "CartesianLeftUnitorInverse using CartesianDiagonal and UniversalMorphismIntoTerminalObject",
+                    [ [ DirectProduct, 1 ],
+                      [ TerminalObject, 1 ],
+                      [ CartesianDiagonalWithGivenCartesianPower, 1 ],
+                      [ UniversalMorphismIntoTerminalObjectWithGivenTerminalObject, 1 ],
+                      [ DirectProductOnMorphismAndObjectWithGivenDirectProducts, 1 ],
+                      [ PreCompose, 1 ] ],
+                    
+  function( cat, a, txa )
+    local L, axa, t;
+    
+    L := ListWithIdenticalEntries( 2, a );
+    
+    axa := DirectProduct( cat, L );
+    
+    t := TerminalObject( cat );
+    
+    return PreCompose( cat,
+                   CartesianDiagonalWithGivenCartesianPower( cat,
+                           a,
+                           2,
+                           axa ),
+                   DirectProductOnMorphismAndObjectWithGivenDirectProducts( cat,
+                           axa,
+                           UniversalMorphismIntoTerminalObjectWithGivenTerminalObject( cat, a, t ),
+                           a,
+                           txa ) );
+    
+end );
+
+##
+AddDerivationToCAP( CartesianRightUnitorInverseWithGivenDirectProduct,
+                    "CartesianRightUnitorInverse using CartesianDiagonal and UniversalMorphismIntoTerminalObject",
+                    [ [ DirectProduct, 1 ],
+                      [ TerminalObject, 1 ],
+                      [ CartesianDiagonalWithGivenCartesianPower, 1 ],
+                      [ UniversalMorphismIntoTerminalObjectWithGivenTerminalObject, 1 ],
+                      [ DirectProductOnObjectAndMorphismWithGivenDirectProducts, 1 ],
+                      [ PreCompose, 1 ] ],
+                    
+  function( cat, a, axt )
+    local L, axa, t;
+    
+    L := ListWithIdenticalEntries( 2, a );
+    
+    axa := DirectProduct( cat, L );
+    
+    t := TerminalObject( cat );
+    
+    return PreCompose( cat,
+                   CartesianDiagonalWithGivenCartesianPower( cat,
+                           a,
+                           2,
+                           axa ),
+                   DirectProductOnObjectAndMorphismWithGivenDirectProducts( cat,
+                           axa,
+                           a,
+                           UniversalMorphismIntoTerminalObjectWithGivenTerminalObject( cat, a, t ),
+                           axt ) );
+    
+end );
+
 ##
 AddDerivationToCAP( CartesianAssociatorRightToLeftWithGivenDirectProducts,
                     "CartesianAssociatorRightToLeftOfDirectProductsWithGivenDirectProducts using the universal morphism into direct product",

CartesianCategories/gap/CocartesianCategoriesDerivedMethods_extra.gi

@@ -84,6 +84,70 @@ AddDerivationToCAP( CocartesianRightUnitorInverseWithGivenCoproduct,
 
 end );
 
+##
+AddDerivationToCAP( CocartesianLeftUnitorWithGivenCoproduct,
+                    "CocartesianLeftUnitor using CocartesianCodiagonal and UniversalMorphismIntoInitialObject",
+                    [ [ Coproduct, 1 ],
+                      [ InitialObject, 1 ],
+                      [ CocartesianCodiagonalWithGivenCocartesianMultiple, 1 ],
+                      [ UniversalMorphismFromInitialObjectWithGivenInitialObject, 1 ],
+                      [ CoproductOnMorphismAndObjectWithGivenCoproducts, 1 ],
+                      [ PreCompose, 1 ] ],
+                    
+  function( cat, a, ixa )
+    local L, axa, i;
+    
+    L := ListWithIdenticalEntries( 2, a );
+    
+    axa := Coproduct( cat, L );
+    
+    i := InitialObject( cat );
+    
+    return PreCompose( cat,
+                   CoproductOnMorphismAndObjectWithGivenCoproducts( cat,
+                           ixa,
+                           UniversalMorphismFromInitialObjectWithGivenInitialObject( cat, a, i ),
+                           a,
+                           axa ),
+                   CocartesianCodiagonalWithGivenCocartesianMultiple( cat,
+                           a,
+                           2,
+                           axa ) );
+    
+end );
+
+##
+AddDerivationToCAP( CocartesianRightUnitorWithGivenCoproduct,
+                    "CocartesianRightUnitor using CocartesianCodiagonal and UniversalMorphismIntoInitialObject",
+                    [ [ Coproduct, 1 ],
+                      [ InitialObject, 1 ],
+                      [ CocartesianCodiagonalWithGivenCocartesianMultiple, 1 ],
+                      [ UniversalMorphismFromInitialObjectWithGivenInitialObject, 1 ],
+                      [ CoproductOnObjectAndMorphismWithGivenCoproducts, 1 ],
+                      [ PreCompose, 1 ] ],
+                    
+  function( cat, a, axi )
+    local L, axa, i;
+    
+    L := ListWithIdenticalEntries( 2, a );
+    
+    axa := Coproduct( cat, L );
+    
+    i := InitialObject( cat );
+    
+    return PreCompose( cat,
+                   CoproductOnObjectAndMorphismWithGivenCoproducts( cat,
+                           axi,
+                           a,
+                           UniversalMorphismFromInitialObjectWithGivenInitialObject( cat, a, i ),
+                           axa ),
+                   CocartesianCodiagonalWithGivenCocartesianMultiple( cat,
+                           a,
+                           2,
+                           axa ) );
+    
+end );
+
 ##
 AddDerivationToCAP( CocartesianAssociatorLeftToRightWithGivenCoproducts,
                     "CocartesianAssociatorLeftToRightWithGivenCoproducts using the universal morphism from coproduct",