Currently, there are several ways to provide the proof of a property of a category (or a functor):
- (C) directly within CatDat
- (M) cite MSE or MO
- (P) cite a paper, book, or another form of publication
Examples.
There are even two suboptions of (C), namely a direct proof in the popup or a dedicated content page, but that is a separate issue and not relevant here. (In fact, there used to be four suboptions, including lemmas and PDFs, but those have already been removed.)
My main question is the following:
Which sources should be preferred? Do we want a fixed preference order?
A natural initial guess would be:
The reasoning is that publications are generally stable, peer-reviewed, and considered the most reliable form of reference.
However, there is a serious issue with this ordering: accessibility. I am not affiliated with a university, and I assume that many users of CatDat are in a similar situation. This means that access to academic literature is restricted, making it impossible to read the referenced proofs.
Also, in terms of user experience, and in particular speed and ease of verification, (C) is clearly best: the proof is immediately available without any external lookup.
In some cases, proofs are too long to include in (C). In such situations, it is very convenient if there already exists a well-written thread on MSE or MO that can simply be cited. Maybe the preference order also depends on the proof length?
However, there is also a major drawback with citations to MSE, MO, or similar platforms: link rot and content volatility. Posts can be deleted or edited at any time by their authors, which means that a reference in CatDat may silently become invalid. This is particularly problematic because such failures are not easily detectable. There is no automated alert that the reference has disappeared or changed.
Taking all of this into account, maybe a better preference order would be:
But even if we agree on such an ordering, it is still unclear whether we should allow direct copying of proofs from MSE or MO into CatDat.
A related question is therefore:
Should we disallow one of the mentioned source types?
Relevant in this context is Keith Kearnes' answer at https://mathoverflow.net/a/509262/2841, which argues that CatDat should prefer references to original publications. This raises another issue: if we include a proof in CatDat, should we attempt to trace its earliest occurrence in the literature? Similarly, if we cite a proof, should we always cite the earliest known source? If so, this quickly becomes a difficult task.
Currently, there are several ways to provide the proof of a property of a category (or a functor):
Examples.
There are even two suboptions of (C), namely a direct proof in the popup or a dedicated content page, but that is a separate issue and not relevant here. (In fact, there used to be four suboptions, including lemmas and PDFs, but those have already been removed.)
My main question is the following:
Which sources should be preferred? Do we want a fixed preference order?
A natural initial guess would be:
The reasoning is that publications are generally stable, peer-reviewed, and considered the most reliable form of reference.
However, there is a serious issue with this ordering: accessibility. I am not affiliated with a university, and I assume that many users of CatDat are in a similar situation. This means that access to academic literature is restricted, making it impossible to read the referenced proofs.
Also, in terms of user experience, and in particular speed and ease of verification, (C) is clearly best: the proof is immediately available without any external lookup.
In some cases, proofs are too long to include in (C). In such situations, it is very convenient if there already exists a well-written thread on MSE or MO that can simply be cited. Maybe the preference order also depends on the proof length?
However, there is also a major drawback with citations to MSE, MO, or similar platforms: link rot and content volatility. Posts can be deleted or edited at any time by their authors, which means that a reference in CatDat may silently become invalid. This is particularly problematic because such failures are not easily detectable. There is no automated alert that the reference has disappeared or changed.
Taking all of this into account, maybe a better preference order would be:
But even if we agree on such an ordering, it is still unclear whether we should allow direct copying of proofs from MSE or MO into CatDat.
A related question is therefore:
Should we disallow one of the mentioned source types?
Relevant in this context is Keith Kearnes' answer at https://mathoverflow.net/a/509262/2841, which argues that CatDat should prefer references to original publications. This raises another issue: if we include a proof in CatDat, should we attempt to trace its earliest occurrence in the literature? Similarly, if we cite a proof, should we always cite the earliest known source? If so, this quickly becomes a difficult task.