Add proof references (WIP)

[ScriptRaccoon]

This is another attempt at #301, at least for a (substantial) sub-problem of it. Specifically, this PR adds proof references (along with proof labels) and therefore prevents proofs from referencing proofs that have been removed (for example, when an implication is added that handles it) or significantly altered; cf. 4041ddb for an example where this has happened.

59 labels and 100 references have been added.

Example usage

The proof that the simplex category $\Delta$ is cosifted now has a label delta_cosifted:

  - property: cosifted
    proof: Let $X,Y \in \Delta$. We may pick [...]
    label: delta_cosifted

The proof for the walking coreflexive pair is now formally referencing it like so:

  - property: cosifted
    proof: Our proof that the <a href="/category/Delta">simplex category</a> is cosifted has only used $[0],[1]$ as auxiliary objects and therefore also shows that $\Delta^{\leq 1}$ is cosifted.
    references:
      - delta_cosifted

How to maintain references

The proofs that reference a given proof can easily be found in the code editor by searching for its (unique) label. They are also stored in the new proof_references table. This table has a foreign key constraint on the property_assignments table, specifically the new label column, which is how the references are verified. In other words, SQL ensures the integrity of the data.

If a proof is changed significantly, we can now check (via the aforementioned search) whether all proofs referencing it still make sense. We might even change the label of the proof. If a proof with a label is removed, we need to fix the proofs that reference it. This was already necessary before, of course, but now we know exactly which proofs are affected.

Other dependencies

This PR does not guard against the case where a previously assigned property turns out to be wrong (this was the main goal of the closed PR #301), but this should be prevented by a good review process. Alternatively, we can handle this in a later PR.

For example, the proof that Ring does not have cofiltered-limit-stable epimorphisms references the fact that CRing does not have cofiltered-limit-stable epimorphisms, but this is not handled by this PR. One can argue that this is also not necessary, or at least much less important than proofs that actually reference other proofs. For example, the proof that Man does not have $\aleph_1$-cofiltered limits literally continues the proof for Set_c, so it needs to be checked that the latter exists and continues to exist.

Finding references

Since it was already very common to reference a proof via a link to the category page, the following query could be used to find proofs that potentially reference other proofs:

select structure_id, property_id from property_assignments where proof like '%/category%' and is_deduced = FALSE;

For functors and morphisms, a similar query works. But still, much manual work was necessary. Also, it is likely that some (few) references have not been recorded yet.