simplified Cartesian*UnitorInverse and Cocartesian*Unitor

Author: mohamed-barakat

CartesianCategories/gap/CartesianCategoriesDerivedMethods_extra.gi

@@ -86,65 +86,45 @@ end );
 
 ##
 AddDerivationToCAP( CartesianLeftUnitorInverseWithGivenDirectProduct,
-                    "CartesianLeftUnitorInverse using CartesianDiagonal and UniversalMorphismIntoTerminalObject",
-                    [ [ DirectProduct, 1 ],
-                      [ TerminalObject, 1 ],
-                      [ CartesianDiagonalWithGivenCartesianPower, 1 ],
+                    "CartesianLeftUnitorInverse using UniversalMorphismIntoTerminalObject and UniversalMorphismIntoDirectProduct",
+                    [ [ TerminalObject, 1 ],
                       [ UniversalMorphismIntoTerminalObjectWithGivenTerminalObject, 1 ],
-                      [ DirectProductOnMorphismAndObjectWithGivenDirectProducts, 1 ],
-                      [ PreCompose, 1 ] ],
+                      [ IdentityMorphism, 1 ],
+                      [ UniversalMorphismIntoDirectProductWithGivenDirectProduct, 1 ] ],
 
   function( cat, a, txa )
-    local L, axa, t;
-    
-    L := ListWithIdenticalEntries( 2, a );
-    
-    axa := DirectProduct( cat, L );
+    local t;
 
     t := TerminalObject( cat );
 
-    return PreCompose( cat,
-                   CartesianDiagonalWithGivenCartesianPower( cat,
-                           a,
-                           2,
-                           axa ),
-                   DirectProductOnMorphismAndObjectWithGivenDirectProducts( cat,
-                           axa,
-                           UniversalMorphismIntoTerminalObjectWithGivenTerminalObject( cat, a, t ),
-                           a,
-                           txa ) );
+    return UniversalMorphismIntoDirectProductWithGivenDirectProduct( cat,
+                   [ t, a ],
+                   a,
+                   [ UniversalMorphismIntoTerminalObjectWithGivenTerminalObject( cat, a, t ),
+                     IdentityMorphism( cat, a ) ],
+                   txa );
 
 end );
 
 ##
 AddDerivationToCAP( CartesianRightUnitorInverseWithGivenDirectProduct,
-                    "CartesianRightUnitorInverse using CartesianDiagonal and UniversalMorphismIntoTerminalObject",
-                    [ [ DirectProduct, 1 ],
-                      [ TerminalObject, 1 ],
-                      [ CartesianDiagonalWithGivenCartesianPower, 1 ],
+                    "CartesianRightUnitorInverse using UniversalMorphismIntoTerminalObject and UniversalMorphismIntoDirectProduct",
+                    [ [ TerminalObject, 1 ],
+                      [ IdentityMorphism, 1 ],
                       [ UniversalMorphismIntoTerminalObjectWithGivenTerminalObject, 1 ],
-                      [ DirectProductOnObjectAndMorphismWithGivenDirectProducts, 1 ],
-                      [ PreCompose, 1 ] ],
+                      [ UniversalMorphismIntoDirectProductWithGivenDirectProduct, 1 ] ],
 
   function( cat, a, axt )
-    local L, axa, t;
-    
-    L := ListWithIdenticalEntries( 2, a );
-    
-    axa := DirectProduct( cat, L );
+    local t;
 
     t := TerminalObject( cat );
 
-    return PreCompose( cat,
-                   CartesianDiagonalWithGivenCartesianPower( cat,
-                           a,
-                           2,
-                           axa ),
-                   DirectProductOnObjectAndMorphismWithGivenDirectProducts( cat,
-                           axa,
-                           a,
-                           UniversalMorphismIntoTerminalObjectWithGivenTerminalObject( cat, a, t ),
-                           axt ) );
+    return UniversalMorphismIntoDirectProductWithGivenDirectProduct( cat,
+                   [ a, t ],
+                   a,
+                   [ IdentityMorphism( cat, a ),
+                     UniversalMorphismIntoTerminalObjectWithGivenTerminalObject( cat, a, t ) ],
+                   axt );
 
 end );
 

CartesianCategories/gap/CocartesianCategoriesDerivedMethods_extra.gi

@@ -86,65 +86,45 @@ end );
 
 ##
 AddDerivationToCAP( CocartesianLeftUnitorWithGivenCoproduct,
-                    "CocartesianLeftUnitor using CocartesianCodiagonal and UniversalMorphismIntoInitialObject",
-                    [ [ Coproduct, 1 ],
-                      [ InitialObject, 1 ],
-                      [ CocartesianCodiagonalWithGivenCocartesianMultiple, 1 ],
+                    "CocartesianLeftUnitor using UniversalMorphismIntoInitialObject and UniversalMorphismFromCoproduct",
+                    [ [ InitialObject, 1 ],
                       [ UniversalMorphismFromInitialObjectWithGivenInitialObject, 1 ],
-                      [ CoproductOnMorphismAndObjectWithGivenCoproducts, 1 ],
-                      [ PreCompose, 1 ] ],
+                      [ IdentityMorphism, 1 ],
+                      [ UniversalMorphismFromCoproductWithGivenCoproduct, 1 ] ],
 
   function( cat, a, ixa )
-    local L, axa, i;
-    
-    L := ListWithIdenticalEntries( 2, a );
-    
-    axa := Coproduct( cat, L );
+    local i;
 
     i := InitialObject( cat );
 
-    return PreCompose( cat,
-                   CoproductOnMorphismAndObjectWithGivenCoproducts( cat,
-                           ixa,
-                           UniversalMorphismFromInitialObjectWithGivenInitialObject( cat, a, i ),
-                           a,
-                           axa ),
-                   CocartesianCodiagonalWithGivenCocartesianMultiple( cat,
-                           a,
-                           2,
-                           axa ) );
+    return UniversalMorphismFromCoproductWithGivenCoproduct( cat,
+                   [ i, a ],
+                   a,
+                   [ UniversalMorphismFromInitialObjectWithGivenInitialObject( cat, a, i ),
+                     IdentityMorphism( cat, a ) ],
+                   ixa );
 
 end );
 
 ##
 AddDerivationToCAP( CocartesianRightUnitorWithGivenCoproduct,
-                    "CocartesianRightUnitor using CocartesianCodiagonal and UniversalMorphismIntoInitialObject",
-                    [ [ Coproduct, 1 ],
-                      [ InitialObject, 1 ],
-                      [ CocartesianCodiagonalWithGivenCocartesianMultiple, 1 ],
+                    "CocartesianRightUnitor using UniversalMorphismIntoInitialObject and UniversalMorphismFromCoproduct",
+                    [ [ InitialObject, 1 ],
+                      [ IdentityMorphism, 1 ],
                       [ UniversalMorphismFromInitialObjectWithGivenInitialObject, 1 ],
-                      [ CoproductOnObjectAndMorphismWithGivenCoproducts, 1 ],
-                      [ PreCompose, 1 ] ],
+                      [ UniversalMorphismFromCoproductWithGivenCoproduct, 1 ] ],
 
   function( cat, a, axi )
-    local L, axa, i;
-    
-    L := ListWithIdenticalEntries( 2, a );
-    
-    axa := Coproduct( cat, L );
+    local i;
 
     i := InitialObject( cat );
 
-    return PreCompose( cat,
-                   CoproductOnObjectAndMorphismWithGivenCoproducts( cat,
-                           axi,
-                           a,
-                           UniversalMorphismFromInitialObjectWithGivenInitialObject( cat, a, i ),
-                           axa ),
-                   CocartesianCodiagonalWithGivenCocartesianMultiple( cat,
-                           a,
-                           2,
-                           axa ) );
+    return UniversalMorphismFromCoproductWithGivenCoproduct( cat,
+                   [ a, i ],
+                   a,
+                   [ IdentityMorphism( cat, a ),
+                     UniversalMorphismFromInitialObjectWithGivenInitialObject( cat, a, i ) ],
+                   axi );
 
 end );