A question for everyone working on CatDat or who is interested to work on it in the future:
Should the input of categorical data be done via markdown files? Here is how it could look like for the category of Banach spaces (excerpt).
# Ban
## summary
id: Ban
notation: $\Ban$
objects: Banach spaces over $\IC$
morphisms: linear contractions (norm ≤ 1)
description: The choice of morphisms is similar to $\Met$, yielding better categorical properties.
nlab_link: https://ncatlab.org/nlab/show/Banach+space
---
## satisfied properties
### locally small
reason: There is a forgetful functor $\Ban \to \Set$ and $\Set$ is locally small.
### pointed
reason: The trivial Banach space $\{0\}$ is a zero object.
## unsatisfied properties
### balanced
reason: The map $x \mapsto x/2$ on $\IC$ is bijective but not isometric, hence not an isomorphism in $\Ban$.
### CSP
reason: The canonical map $\coprod \IC \to \prod \IC$ corresponds to $\ell^1 \to \ell^\infty$, which is not epimorphic since its closure is $c_0$.
---
## special morphisms
### monomorphisms
description: injective linear contractions
reason: The unit ball functor $U : \Ban \to \Set$ is faithful and representable (by $\IC$), hence reflects and preserves monomorphisms.
The markdown file could then be parsed to a SQL file, or directly used to insert SQL. This is an extra development, might lead to parsing issues one needs to solve, but maybe it's justified when adding the data becomes easier for contributors and there is no weird SQL syntax in our way anymore?
Notice that something similar is used in Pi-Base.
The approach would also bring the data of a single category closer together, in just one file. This could also be done in the current setup with SQL files, but it would produce much more query boilerplate; the markdown approach is more suitable for that.
If we do it for categories, then it should also be done with all the other data (properties, implications, lemmas, functors, etc.).
A question for everyone working on CatDat or who is interested to work on it in the future:
Should the input of categorical data be done via markdown files? Here is how it could look like for the category of Banach spaces (excerpt).
The markdown file could then be parsed to a SQL file, or directly used to insert SQL. This is an extra development, might lead to parsing issues one needs to solve, but maybe it's justified when adding the data becomes easier for contributors and there is no weird SQL syntax in our way anymore?
Notice that something similar is used in Pi-Base.
The approach would also bring the data of a single category closer together, in just one file. This could also be done in the current setup with SQL files, but it would produce much more query boilerplate; the markdown approach is more suitable for that.
If we do it for categories, then it should also be done with all the other data (properties, implications, lemmas, functors, etc.).