test TruthMorphismOfImplies

needs Toposes v2021.11-10

Author: mohamed-barakat

PackageInfo.g

@@ -10,7 +10,7 @@ SetPackageInfo( rec(
 
 PackageName := "FinSetsForCAP",
 Subtitle := "The elementary topos of (skeletal) finite sets",
-Version := "2020.11-09",
+Version := "2020.11-10",
 
 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-09" ],
+                   [ "Toposes", ">= 2021.11-10" ],
                    ],
   SuggestedOtherPackages := [ ],
   ExternalConditions := [ ],

examples/SubobjectClassifier.g

@@ -2,6 +2,10 @@
 
 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 ] );
 #! <An object in FinSets>
@@ -28,6 +32,12 @@ Display( TruthMorphismOfOr( FinSets ) );
 #!   [ [ [ "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" ] ]
 m := MapOfFinSets( A, List( AsList( A ), x -> [ x, x ] ), S );
 #! <A morphism in FinSets>
 Display( ClassifyingMorphismOfSubobject( m ) );