All properties in the database should eventually have a dual. Only then does the deduction system work fully*. Moreover, although a property's dual may be less common, it corresponds to a common property of the dual category and is therefore interesting in its own right.
From now on, every new property should have a dual. Any PR adding a property P must also add Pop.
The following properties currently do not have a dual.
| ID |
Type |
| Grothendieck abelian |
category |
| Grothendieck topos |
category |
| ℵ₁-accessible |
category |
| elementary topos |
category |
| finitary algebraic |
category |
| finitely accessible |
category |
| generalized variety |
category |
| locally ℵ₁-presentable |
category |
| locally finitely multi-presentable |
category |
| locally finitely presentable |
category |
| locally multi-presentable |
category |
| locally poly-presentable |
category |
| multi-algebraic |
category |
| natural numbers object |
category |
| one-sorted finitary algebraic |
category |
| parametrized natural numbers object |
category |
| pretopos |
category |
| quasitopos |
category |
| representable |
functor |
| well-pointed |
symmetric_monoidal_category |
Query:
SELECT id, type FROM properties WHERE dual_property_id IS NULL;
Maybe "representable functors" cannot be dualized since their target is fixed. In any case, the focus should be on categories.
For each added dual property, it should be decided for as many categories as possible whether they satisfy it or not. In many cases, this is already done via the deduction system, which automatically dualizes implications. For example, when adding "co-natural numbers object" and "parametrized co-natural numbers object", the first property is automatically decided for all categories in the database, while the second only remains to be decided for the category of (commutative) algebras (and the category of (commutative) rings).
*A typical situation is the following. We have properties with duals P, Q and an implication P => Q. It gets dualized automatically. We add a new property R which has not a dual yet and add this as a conclusion of the implication: P => Q and R. But now, it does not get dualized anymore. Thus, we are losing Pop => Qop. We need to make this a separate implication: P => R. This has been forgotten a couple of times (for example, when $\aleph_1$-accessible was added).
Another issue appears in walking_coreflexive_pair.yaml where the proof of the negation of multi-complete has to be done manually just because locally multi-presentable has not yet been dualized.
There is also a comment for the implication finite_filtered_colimits that needs to be addressed when we add "finitely coaccessible".
All properties in the database should eventually have a dual. Only then does the deduction system work fully*. Moreover, although a property's dual may be less common, it corresponds to a common property of the dual category and is therefore interesting in its own right.
From now on, every new property should have a dual. Any PR adding a property P must also add Pop.
The following properties currently do not have a dual.
Query:
Maybe "representable functors" cannot be dualized since their target is fixed. In any case, the focus should be on categories.
For each added dual property, it should be decided for as many categories as possible whether they satisfy it or not. In many cases, this is already done via the deduction system, which automatically dualizes implications. For example, when adding "co-natural numbers object" and "parametrized co-natural numbers object", the first property is automatically decided for all categories in the database, while the second only remains to be decided for the category of (commutative) algebras (and the category of (commutative) rings).
*A typical situation is the following. We have properties with duals P, Q and an implication P => Q. It gets dualized automatically. We add a new property R which has not a dual yet and add this as a conclusion of the implication: P => Q and R. But now, it does not get dualized anymore. Thus, we are losing Pop => Qop. We need to make this a separate implication: P => R. This has been forgotten a couple of times (for example, when$\aleph_1$ -accessible was added).
Another issue appears in
walking_coreflexive_pair.yamlwhere the proof of the negation ofmulti-completehas to be done manually just becauselocally multi-presentablehas not yet been dualized.There is also a comment for the implication
finite_filtered_colimitsthat needs to be addressed when we add "finitely coaccessible".