added SubobjectClassifier for SkeletalFinSets

Author: mohamed-barakat

PackageInfo.g

@@ -10,7 +10,7 @@ SetPackageInfo( rec(
 
 PackageName := "FinSetsForCAP",
 Subtitle := "The elementary topos of (skeletal) finite sets",
-Version := "2020.11-12",
+Version := "2020.11-13",
 
 Date := Concatenation( "01/", ~.Version{[ 6, 7 ]}, "/", ~.Version{[ 1 .. 4 ]} ),
 License := "GPL-2.0-or-later",

doc/Doc.autodoc

@@ -119,3 +119,6 @@
 
 @Subsection Skeletal topos properties
 @InsertChunk SkeletalTopos
+
+@Subsection Skeletal Subobject Classifier
+@InsertChunk SkeletalSubobjectClassifier

examples/SkeletalSubobjectClassifier.g

@@ -0,0 +1,34 @@
+#! @Chunk SkeletalSubobjectClassifier
+
+LoadPackage( "FinSetsForCAP" );
+
+# Below we see that the internal logic
+# of the category SkeletalFinSets is classical logic,
+# i.e., the topos SkeletalFinSets is Boolean.
+
+#! @Example
+Display( SubobjectClassifier( SkeletalFinSets ) );
+#! 2
+Display( TruthMorphismOfTrue( SkeletalFinSets ) );
+#! [ 1, [ 1 ], 2 ]
+Display( TruthMorphismOfFalse( SkeletalFinSets ) );
+#! [ 1, [ 2 ], 2 ]
+Display( TruthMorphismOfNot( SkeletalFinSets ) );
+#! [ 2, [ 2, 1 ], 2 ]
+Display( CartesianSquareOfSubobjectClassifier( SkeletalFinSets ) );
+#! 4
+Display( TruthMorphismOfAnd( SkeletalFinSets ) );
+#! [ 4, [ 1, 2, 2, 2 ], 2 ]
+Display( TruthMorphismOfOr( SkeletalFinSets ) );
+#! [ 4, [ 1, 1, 1, 2 ], 2 ]
+Display( TruthMorphismOfImplies( SkeletalFinSets ) );
+#! [ 4, [ 1, 2, 1, 1 ], 2 ]
+S := FinSet( 5 );
+#! <An object in SkeletalFinSets>
+A := FinSet( 2 );
+#! <An object in SkeletalFinSets>
+m := MapOfFinSets( A, [ 1, 5 ], S );
+#! <A morphism in SkeletalFinSets>
+Display( ClassifyingMorphismOfSubobject( m ) );
+#! [ 5, [ 1, 2, 2, 2, 1 ], 2 ]
+#! @EndExample

gap/SkeletalFinSetsForCAP.gi

@@ -777,6 +777,36 @@ AddCartesianEvaluationMorphismWithGivenSource( SkeletalFinSets,
 
 end );
 
+##
+AddSubobjectClassifier( SkeletalFinSets,
+  function ( cat )
+      
+      return FinSet( cat, 2 );
+      
+end );
+
+##
+AddClassifyingMorphismOfSubobjectWithGivenSubobjectClassifier( SkeletalFinSets,
+  function ( cat, monomorphism, Omega )
+    local range, images;
+    
+    range := Range( monomorphism );
+    
+    images := List( range,
+                    function ( x )
+                      
+                      if x in AsList( monomorphism ) then
+                          return 1;
+                      fi;
+                      
+                      return 2;
+                      
+                  end );
+      
+      return MapOfFinSets( range, images, Omega );
+      
+end );
+
 end );
 
 ##