Turn UniqueMorphism into a CAP operation

[homalg-project]

Turn UniqueMorphism into a CAP operation

[mohamed-barakat]

Together with @zickgraf we decided to turn UniqueMorphism into a CAP operation :)

[mohamed-barakat]

The content of the various ADD_COMMON_METHODS_FOR_* in Locales can then be turned into derivations, and these global functions should be deleted. This should resolve two issues one issue:

• setting the wrong properties for TerminalCategoriesWithMultipleObjects mentioned in homalg-project/CAP_project#1039 and affecting homalg-project/CAP_project#1009;
• get these trivial CAP operations for morphisms in a thin category out of the list of primitively installed operations, so they do not appear in the list of compiled primitive operations.

[zickgraf]

Regarding the first point: Would you get rid of the involved properties completely? If yes, why can't you do this already now? If no, how would this solve setting the wrong properties for TerminalCategoriesWithMultipleObjects?

[mohamed-barakat]

The wrong properties were set by these ADD_COMMON_METHODS_FOR_*. They are currently used to install methods that should in principle be derived, once there is an operation called UniqueMorphism(WithWitness). I wanted to discuss the details with you anyway before changing Locales accordingly.

[mohamed-barakat]

@TKuh: I was wrong, I don't use ADD_COMMON_METHODS_FOR_* in the terminal category constructor.