Remove IsCongruentForMorphisms from the record entry EveryCategory

[mohamed-barakat]

I suggest removing IsCongruentForMorphisms from CAP_INTERNAL_CONSTRUCTIVE_CATEGORIES_RECORD.EveryCategory and adding it to a new record entry of CAP_INTERNAL_CONSTRUCTIVE_CATEGORIES_RECORD. I can think of two possible names for this algorithmic property:

• IsCategoryWithDecidableEqualityOfMorphisms
• IsComputableCategory

[zickgraf]

I guess your application is that you do not want to lose constructivity of all the constructions for non-computable categories? The point is that the specifications for the constructions all include the congruence. Additionally, removing IsCongruentForMorphisms from EveryCategory is probably not enough: IsAbCategory also requires IsZeroForMorphisms which will give the same problem.

But of course I see the application. I suggest to let InfoString... handle non-computable categories explicitly instead. It could then print something like "non-decidabely constructive".

More generally, non-computable categories are no first-class citizens of CAP currently. With the changes regarding the equalities which I currently implement, they can become first-class citizens in the future. In particular, if we derive IsEqual... automatically from the object/morphism data and tell the user to implement IsCongruentForMorphisms explicitly instead of deriving it from IsEqualForMorphisms, we can actually take the existence of IsCongruentForMorphisms as an indicator for computability, instead of relying on an undocumented flag. But this will need some more time and discussions, so currently we have to live with some workarounds.

[mohamed-barakat]

I guess your application is that you do not want to lose constructivity of all the constructions for non-computable categories?

Yes.

The point is that the specifications for the constructions all include the congruence. Additionally, removing IsCongruentForMorphisms from EveryCategory is probably not enough: IsAbCategory also requires IsZeroForMorphisms which will give the same problem.

True, I missed this one. After a quick search, I don't see more.

But of course I see the application. I suggest to let InfoString... handle non-computable categories explicitly instead. It could then print something like "non-decidabely constructive".

Yes, the "non-computability" (or a another name) should be added to InfoString...

More generally, non-computable categories are no first-class citizens of CAP currently. With the changes regarding the equalities which I currently implement, they can become first-class citizens in the future. In particular, if we derive IsEqual... automatically from the object/morphism data and tell the user to implement IsCongruentForMorphisms explicitly instead of deriving it from IsEqualForMorphisms, we can actually take the existence of IsCongruentForMorphisms as an indicator for computability, instead of relying on an undocumented flag. But this will need some more time and discussions, so currently we have to live with some workarounds.

Very nice. I agree.