Group properties with their dual on the properties page

[varkor]

It would be convenient to group properties together with their dual (when it exists in CatDat). E.g. having a single bullet point for "complete" and "cocomplete" (e.g. separated by a forward slash, or something like this). This would shorten the list of properties considerably and make it more convenient to search for a property (as well as avoiding the current issue that there is a huge sequence of properties starting with "co-" in the list).

[ScriptRaccoon]

I am afraid this is not possible since the deduced properties are written in a particular order. If P uses A and B, then A and B need to deduced before on the page, meaning, above it in the list. Otherwise as a reader one would have to go back and forth, it would be very confusing since deductions can take a long way.

One could offer a separate view though where the reasons are not displayed and hence the order does not matter. Then the grouping would also be available. But I don't like this idea either.

I think the actual issue would be to offer a search feature on the detail page. But do we need this? On the browser just use Command + F and input the property.

EDIT. This reply was based on a misunderstanding. Sorry

[varkor]

I specifically mean on https://catdat.app/category-properties, not on the individual categories pages.

[ScriptRaccoon]

💡

[ScriptRaccoon]

@varkor What is the expected action when a user uses the search and inputs "cofiltered". Should this display the row which has "filtered colimits / cofiltered limits"? Should it remove the first part of it?

[varkor]

I think whichever option is easiest to implement would be fine. I don't think it would be confusing or inconvenient to show the entire row, for instance.

[ScriptRaccoon]

This really shines when combined with the filtering.