AddCartesianCoevaluationMorphismWithGivenRange( SkeletalFinSets, ... )

Author: mohamed-barakat

doc/Doc.autodoc

@@ -112,6 +112,9 @@
 @Subsection Skeletal Pushout
 @InsertChunk SkeletalPushout
 
+@Subsection Skeletal Cartesian Lambda Introduction
+@InsertChunk SkeletalCartesianLambdaIntroduction
+
 @Subsection Skeletal Lift
 @InsertChunk SkeletalLift
 

examples/SkeletalCartesianLambdaIntroduction.g

@@ -0,0 +1,30 @@
+#! @Chunk SkeletalCartesianLambdaIntroduction
+
+LoadPackage( "FinSetsForCAP" );
+
+#! @Example
+S := FinSet( 3 );
+#! <An object in SkeletalFinSets>
+R := FinSet( 2 );
+#! <An object in SkeletalFinSets>
+f := MapOfFinSets( S, [ 2, 2, 1 ], R );
+#! <A morphism in SkeletalFinSets>
+IsWellDefined( f );
+#! true
+T := TerminalObject( SkeletalFinSets );
+#! <An object in SkeletalFinSets>
+IsTerminal( T );
+#! true
+lf := CartesianLambdaIntroduction( f );
+#! <A split monomorphism in SkeletalFinSets>
+Source( lf ) = T;
+#! true
+Display( Range( lf ) );
+#! 8
+Display( lf );
+#! [ 1, [ 7 ], 8 ]
+elf := CartesianLambdaElimination( S, R, lf );
+#! <A morphism in SkeletalFinSets>
+elf = f;
+#! true
+#! @EndExample

examples/SkeletalTopos.g

@@ -31,5 +31,20 @@ CartesianBraidingInverse( M, N );;
 ExponentialOnObjects( M, N );;
 ExponentialOnMorphisms( f, g );;
 CartesianEvaluationMorphism( M, N );;
+CartesianCoevaluationMorphism( M, N );;
+DirectProductToExponentialAdjunctionMap( M, N,
+    UniversalMorphismIntoTerminalObject( DirectProduct( M, N ) )
+);;
+ExponentialToDirectProductAdjunctionMap( M, N,
+    UniversalMorphismFromInitialObject( ExponentialOnObjects( M, N ) )
+);;
+
+M := FinSet( 2 );;
+N := FinSet( 2 );;
+P := FinSet( 1 );;
+Q := FinSet( 2 );;
+CartesianPreComposeMorphism( M, N, P );;
+CartesianPostComposeMorphism( M, N, P );;
+DirectProductExponentialCompatibilityMorphism( [ M, N, P, Q ] );;
 
 #! @EndExample

examples/Topos.g

@@ -45,6 +45,6 @@ P := FinSet( [ "*" ] );;
 Q := FinSet( [ "§", "&" ] );;
 CartesianPreComposeMorphism( M, N, P );;
 CartesianPostComposeMorphism( M, N, P );;
-DirectProductExponentialCompatibilityMorphism( [ M, N, P, Q  ] );;
+DirectProductExponentialCompatibilityMorphism( [ M, N, P, Q ] );;
 
 #! @EndExample

gap/SkeletalFinSetsForCAP.gi

@@ -841,6 +841,18 @@ AddCartesianEvaluationMorphismWithGivenSource( SkeletalFinSets,
 
 end );
 
+##
+AddCartesianCoevaluationMorphismWithGivenRange( SkeletalFinSets,
+  function ( cat, M, N, HN_MxN )
+    local m, n;
+    
+    m := Length( M );
+    n := Length( N );
+    
+    return MapOfFinSets( M, List( [ 0 .. m - 1 ], i -> 1 + Sum( [ 0 .. n - 1 ], j -> ( i * n + j ) * (m*n)^(n - j - 1) ) ), HN_MxN );
+    
+end );
+
 ##
 AddSubobjectClassifier( SkeletalFinSets,
   function ( cat )

gap/precompiled_categories/CategoryOfSkeletalFinSetsPrecompiled.gi

@@ -22,6 +22,29 @@ end
 
     , 100 );
 
+    ##
+    AddCartesianCoevaluationMorphismWithGivenRange( cat,
+        
+########
+function ( cat_1, a_1, b_1, r_1 )
+    local hoisted_1_1, hoisted_2_1, hoisted_3_1, deduped_4_1, deduped_5_1;
+    deduped_5_1 := Length( b_1 );
+    deduped_4_1 := Length( a_1 );
+    hoisted_3_1 := [ 0 .. deduped_5_1 - 1 ];
+    hoisted_2_1 := deduped_4_1 * deduped_5_1;
+    hoisted_1_1 := deduped_5_1;
+    return MapOfFinSets( a_1, List( [ 0 .. deduped_4_1 - 1 ], function ( i_2 )
+              local hoisted_1_2;
+              hoisted_1_2 := i_2 * hoisted_1_1;
+              return 1 + Sum( hoisted_3_1, function ( j_3 )
+                        return (hoisted_1_2 + j_3) * hoisted_2_1 ^ (hoisted_1_1 - j_3 - 1);
+                    end );
+          end ), r_1 );
+end
+########
+        
+    , 100 );
+    
     ##
     AddCartesianEvaluationMorphismWithGivenSource( cat,