Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

outsourced a derivation of IsHomSetInhabited from Toposes to FinSetsForCAP #211

Merged
merged 1 commit into from
Jul 3, 2023
Merged

outsourced a derivation of IsHomSetInhabited from Toposes to FinSetsForCAP #211

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion PackageInfo.g
View file
Open in desktop
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
1 change: 1 addition & 0 deletions examples/PrecompileCategoryOfSkeletalFinSetsWithMorphismsGivenByLists.g
View file
Open in desktop
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
View file
Open in desktop
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
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -331,14 +331,6 @@

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

##
AddDerivationToCAP( IsHomSetInhabited,
"IsHomSetInhabited using IsInitial when the range category of the homomorphism structure is the skeletal category of finite sets",
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

General comment which does not block the PR: The information you provide in this description is nearly the same as would be displayed by DerivationsOfMethodByCategory anyway. Unfortunately, this is the case for many descriptions of derivations. It would be more useful if descriptions would describe the mathematics/semantics behind the derivations.

[ [ 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
2 changes: 1 addition & 1 deletion gap/precompiled_categories/CategoryOfSkeletalFinSetsWithMorphismsGivenByListsPrecompiled.gi
View file
Open in desktop
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