Merge pull request #66 from mohamed-barakat/logic

Test internal logic

Author: zickgraf

PackageInfo.g

@@ -10,7 +10,7 @@ SetPackageInfo( rec(
 
 PackageName := "FinSetsForCAP",
 Subtitle := "The elementary topos of (skeletal) finite sets",
-Version := "2020.11-05",
+Version := "2020.11-13",
 
 Date := Concatenation( "01/", ~.Version{[ 6, 7 ]}, "/", ~.Version{[ 1 .. 4 ]} ),
 License := "GPL-2.0-or-later",
@@ -100,7 +100,7 @@ Dependencies := rec(
   NeededOtherPackages := [
                    [ "GAPDoc", ">= 1.5" ],
                    [ "CAP", ">= 2021.05-02" ],
-                   [ "Toposes", ">= 2021.11-05" ],
+                   [ "Toposes", ">= 2021.11-11" ],
                    ],
   SuggestedOtherPackages := [ ],
   ExternalConditions := [ ],

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

examples/SubobjectClassifier.g

@@ -2,17 +2,49 @@
 
 LoadPackage( "FinSetsForCAP" );
 
+# Below we see that the internal logic
+# of the category FinSets is classical logic,
+# i.e., the topos FinSets is Boolean.
+
 #! @Example
-S := FinSet([1,2,3,4,5]);
+Display( SubobjectClassifier( FinSets ) );
+#! [ "true", "false" ]
+Display( TruthMorphismOfTrue( FinSets ) );
+#! [ [ "*" ], [ [ "*", "true" ] ], [ "true", "false" ] ]
+Display( TruthMorphismOfFalse( FinSets ) );
+#! [ [ "*" ], [ [ "*", "false" ] ], [ "true", "false" ] ]
+Display( TruthMorphismOfNot( FinSets ) );
+#! [ [ "true", "false" ],
+#!   [ [ "false", "true" ], [ "true", "false" ] ],
+#!   [ "true", "false" ] ]
+Display( CartesianSquareOfSubobjectClassifier( FinSets ) );
+#! [ [ "true", "true" ], [ "true", "false" ],
+#!   [ "false", "true" ],  [ "false", "false" ] ]
+Display( TruthMorphismOfAnd( FinSets ) );
+#! [ [ [ "true", "true" ], [ "true", "false" ],
+#!     [ "false", "true" ], [ "false", "false" ] ],
+#!   [ [ [ "false", "false" ], "false" ], [ [ "false", "true" ], "false" ],
+#!     [ [ "true", "false" ], "false" ], [ [ "true", "true" ], "true" ] ],
+#!   [ "true", "false" ] ]
+Display( TruthMorphismOfOr( FinSets ) );
+#! [ [ [ "true", "true" ], [ "true", "false" ],
+#!     [ "false", "true" ], [ "false", "false" ] ],
+#!   [ [ [ "false", "false" ], "false" ], [ [ "false", "true" ], "true" ],
+#!    [ [ "true", "false" ], "true" ], [ [ "true", "true" ], "true" ] ],
+#!   [ "true", "false" ] ]
+Display( TruthMorphismOfImplies( FinSets ) );
+#! [ [ [ "true", "true" ], [ "true", "false" ],
+#!     [ "false", "true" ], [ "false", "false" ] ],
+#!   [ [ [ "false", "false" ], "true" ], [ [ "false", "true" ], "true" ],
+#!     [ [ "true", "false" ], "false" ], [ [ "true", "true" ], "true" ] ],
+#!   [ "true", "false" ] ]
+S := FinSet( [ 1, 2, 3, 4, 5 ] );
 #! <An object in FinSets>
-A := FinSet([1,5]);
+A := FinSet( [ 1, 5 ] );
 #! <An object in FinSets>
-m := MapOfFinSets(A, List(AsList(A), x -> [x,x]), S);
-#! <A morphism in FinSets>
-Display(TruthMorphismOfTrue(FinSets));
-#! [ [ "*" ], [ [ "*", "true" ] ], [ "true", "false" ] ]
-Display(ClassifyingMorphismOfSubobject(m));
-#! [ [ 1, 2, 3, 4, 5 ], [ [ 1, "true" ], [ 2, "false" ], [ 3, "false" ], 
+m := EmbeddingOfFinSets( A, S );
+#! <A monomorphism in FinSets>
+Display( ClassifyingMorphismOfSubobject( m ) );
+#! [ [ 1, 2, 3, 4, 5 ], [ [ 1, "true" ], [ 2, "false" ], [ 3, "false" ],
 #! [ 4, "false" ], [ 5, "true" ] ], [ "true", "false" ] ]
-
 #! @EndExample

gap/FinSetsForCAP.gi

@@ -1004,21 +1004,24 @@ end );
 
 ##
 AddClassifyingMorphismOfSubobjectWithGivenSubobjectClassifier( category_of_finite_sets,
-  function ( category_of_finite_sets, monomorphism, omega )
-      local range, image, r, x;
-
-      r := [ ];
-      range := Range( monomorphism );
-
-      for x in range do
-          if x in ImageObject( monomorphism ) then
-              Add( r, [ x, "true" ] );
-          else
-              Add( r, [ x, "false" ] );
-          fi;
-      od;
-            
-      return MapOfFinSets( range, r, omega );
+  function ( category_of_finite_sets, monomorphism, Omega )
+    local range, images;
+    
+    range := Range( monomorphism );
+    
+    images := List( range,
+                    function ( x )
+                      
+                      if x in ImageObject( monomorphism ) then
+                          return [ x, "true" ];
+                      fi;
+                      
+                      return [ x, "false" ];
+                      
+                  end );
+      
+      return MapOfFinSets( range, images, Omega );
+      
 end );
 
 end );

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 );
 
 ##