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).
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).