Show implication usage

[ScriptRaccoon]

Each implication page now shows the categories that use this implication in one of their property assignments. This is similar to the feature for content pages added in #189. It highlights how useful the implications are.

This is implemented by checking whether the reason for a property assignment contains a reference to the implication page (these references are inserted by the deduction script). Thus, this is currently not a formal SQL-level relationship, but it should be sufficient for now.

The list is collapsed by default because it can become quite long.

How it looks like

Collapsed

Expanded

Usage

Separate queries have shown that many implications are used very frequently, in particular equivalences that hold by definition (e.g. Barr-exact_definition). However, there are also implications that are used by only a single category (e.g. equalizers_via_kernels), and sometimes even none at all (e.g. cartesian_closed_thin_criterion).

Redundant implications

In the case of an unused implication, this can indicate that the implication is redundant (follows from others). I therefore checked this using the consistency check in the search page (#170). There are 5 non-deduced implications that are currently unused:

• accessible_locally_small
• cartesian_closed_thin_criterion
• infinite_distributive_filtered_criterion
• strict_initial_right_criterion
• thin_finite_product_reduction

The first three are not redundant. The fourth is redundant and has been removed. The fifth is also redundant, but has been kept because its derivation from other implications is somewhat non-trivial.

Removing redundant implications in general is part of #16.

Functors

The same adjustment has also been made for functor implication pages. Unsurprisingly, since the database currently contains only six functors, many functor implications are still unused.