Introduce IsSafeWellDefinedFor* or IsMathematicallyWellDefinedFor*

[mohamed-barakat]

The current IsWellDefinedForObjects and IsWellDefinedForMorphism include tests for checking whether the type of ObjectDatum/MorphismDatum is correct. They all compile to true.

It would make sense to introduce IsSafeWellDefinedFor* or IsMathematicallyWellDefinedFor* which assumes that these type-check-tests are true and only tests the "mathematical" conditions. Only the latter should be compiled and are relevant in the proof-assistant mode.

[zickgraf]

The current IsWellDefinedForObjects and IsWellDefinedForMorphism include tests for checking whether the type of ObjectDatum/MorphismDatum is correct. They all compile to true.

Could you provide the example(s) you have in mind?

It would make sense to introduce IsSafeWellDefinedFor* or IsMathematicallyWellDefinedFor* which assumes that these type-check-tests are true and only tests the "mathematical" conditions. Only the latter should be compiled and are relevant in the proof-assistant mode.

The explicit type checks in IsWellDefined* are important in proof-assistant mode, otherwise nonsensical statements can reduce to true.

General note: I do not expect that we can always derive a correct IsWellDefined* in the context of reinterpretations. For example, the integer defining an object in the category of rows corresponds to the length of a list in the additive closure. In the context of the category of rows we have to check that the integer is non-negative, but the length of a list is always non-negative, so this check makes no sense in the context of the tower.

[mohamed-barakat]

I resolved this in IsWellDefinedFor* in the constructor CategoryOfMonoids.