Skip to content

Commit

Permalink
outsourced a derivation of IsHomSetInhabited from Toposes to FinSetsF…
Browse files Browse the repository at this point in the history
…orCAP
  • Loading branch information
mohamed-barakat committed Jul 3, 2023
1 parent 519f2e5 commit 09746cd
Show file tree
Hide file tree
Showing 5 changed files with 33 additions and 10 deletions.
2 changes: 1 addition & 1 deletion PackageInfo.g
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ SetPackageInfo( rec(

PackageName := "FinSetsForCAP",
Subtitle := "The elementary topos of (skeletal) finite sets",
Version := "2023.06-05",
Version := "2023.06-06",

Date := (function ( ) if IsBound( GAPInfo.SystemEnvironment.GAP_PKG_RELEASE_DATE ) then return GAPInfo.SystemEnvironment.GAP_PKG_RELEASE_DATE; else return Concatenation( ~.Version{[ 1 .. 4 ]}, "-", ~.Version{[ 6, 7 ]}, "-01" ); fi; end)( ),
License := "GPL-2.0-or-later",
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,7 @@ primitive_operations :=
category_constructor( : no_precompiled_code := true ) );;
list_of_operations :=
SortedList( Concatenation( primitive_operations, [
"IsHomSetInhabited",
"TruthMorphismOfImplies",
#"HasPushoutComplement",
"PushoutComplement",
Expand Down
9 changes: 9 additions & 0 deletions gap/CompilerLogic.gi
Original file line number Diff line number Diff line change
Expand Up @@ -431,6 +431,15 @@ CapJitAddLogicTemplate(
)
);

CapJitAddLogicTemplate(
rec(
variable_names := [ "number1", "number2" ],
variable_filters := [ IsBigInt, IsBigInt ],
src_template := "not number2 ^ number1 = 0",
dst_template := "number1 = 0 or not number2 = 0",
)
);

CapJitAddLogicTemplate(
rec(
variable_names := [ "entry", "func" ],
Expand Down
29 changes: 21 additions & 8 deletions gap/SkeletalFinSets.gi
Original file line number Diff line number Diff line change
Expand Up @@ -331,14 +331,6 @@ AddIsEqualForMorphisms( SkeletalFinSets,

end );

##
AddIsHomSetInhabited( SkeletalFinSets,
function ( cat, A, B )

return IsInitial( cat, A ) or not IsInitial( cat, B );

end );

##
AddIdentityMorphism( SkeletalFinSets,
function ( cat, n )
Expand Down Expand Up @@ -985,6 +977,27 @@ end, 1 + Sum( [ [ "ExponentialOnObjects", 1 ],

end );

##
AddDerivationToCAP( IsHomSetInhabited,
"IsHomSetInhabited using IsInitial when the range category of the homomorphism structure is the skeletal category of finite sets",
[ [ HomomorphismStructureOnObjects, 1 ],
[ IsInitial, 1, RangeCategoryOfHomomorphismStructure ] ],

function ( cat, a, b )
local range_cat;

range_cat := RangeCategoryOfHomomorphismStructure( cat );

Check warning on line 989 in gap/SkeletalFinSets.gi

View check run for this annotation

Codecov / codecov/patch

gap/SkeletalFinSets.gi#L989

Added line #L989 was not covered by tests

return not IsInitial( range_cat,
HomomorphismStructureOnObjects( cat, a, b ) );

Check warning on line 992 in gap/SkeletalFinSets.gi

View check run for this annotation

Codecov / codecov/patch

gap/SkeletalFinSets.gi#L991-L992

Added lines #L991 - L992 were not covered by tests

end : CategoryGetters := rec( range_cat := RangeCategoryOfHomomorphismStructure ),
CategoryFilter :=
function ( cat )
return HasRangeCategoryOfHomomorphismStructure( cat ) and
IsCategoryOfSkeletalFinSets( RangeCategoryOfHomomorphismStructure( cat ) );
end );

##
InstallMethod( String,
"for a CAP skeletal finite set",
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -449,7 +449,7 @@ function ( cat_1, arg2_1, arg3_1 )
end
########

, 100 );
, 202 : IsPrecompiledDerivation := true );

##
AddIsInitial( cat,
Expand Down

0 comments on commit 09746cd

Please sign in to comment.