Input all categorical data via YAML files

[ScriptRaccoon]

All categorical data is now authored in YAML files. Contributors no longer need to touch SQL seed files anymore. YAML is more readable, structured, and independent of the database layer.

To support this change, existing seed data has been converted (once) into YAML. From now on, YAML is the single source of truth for seeded data. The SQL seed files have been deleted, but the SQLite database is kept as before. It is still used for storage, querying, and for running deduction scripts. The schema is still defined in SQL files.

There is a major improvement: each category now has its own YAML file. These files no longer contain only the basic metadata, but also tags, related categories, satisfied and unsatisfied properties of the category, and more (see the example below). This information is no longer distributed across many SQL files, making it much easier to add new categories and maintain existing ones.

The same changes have been made for functors. In addition, each property (of a category or a functor) now has its own YAML file. The implications are still grouped by topic, but the topics have been refined, so each file is now more focused.

Previously, SQL seed files were doing two things at once: defining the data and also implementing the logic to insert and normalize it into multiple tables. This PR separates those concerns. The insertion logic is now handled explicitly in the new seed script, while YAML only defines the data itself. This does introduce an extra layer (YAML parsing + import step), but this layer already existed implicitly before in the SQL seed files.

A challenge was finding a good and consistent way to format long strings used as YAML values. This will likely need further improvement in the future. It was also tested whether Markdown could be used inside fields, but this caused more problems than it solved.

This PR resolves #163 (but with YAML instead of markdown).

Example

Here is the current version Ab.yaml. All the information about this category is in one file.

id: Ab
name: category of abelian groups
notation: $\Ab$
objects: abelian groups
morphisms: group homomorphisms
description: This is the prototype of an abelian category.
nlab_link: https://ncatlab.org/nlab/show/Ab

tags:
  - algebra

related_categories:
  - Ab_fg
  - CMon
  - FinAb
  - FreeAb
  - Grp
  - R-Mod
  - TorsAb
  - TorsFreeAb

satisfied_properties:
  - property_id: locally small
    reason: There is a forgetful functor $\Ab \to \Set$ and $\Set$ is locally small.

  - property_id: abelian
    reason: This is standard, see <a href="https://ncatlab.org/nlab/show/Categories+for+the+Working+Mathematician" target="_blank">Mac Lane</a>, Ch. VIII.

  - property_id: finitary algebraic
    reason: Take the algebraic theory of a commutative group.

unsatisfied_properties:
  - property_id: split abelian
    reason: The short exact sequence $0 \xrightarrow{} \IZ \xrightarrow{p} \IZ \xrightarrow{} \IZ/p \xrightarrow{} 0$ does not split.

  - property_id: skeletal
    reason: This is trivial.

  - property_id: CSP
    reason: The canonical homomorphism $\bigoplus_{n \geq 0} \IZ \to \prod_{n \geq 0} \IZ$ is not surjective, hence no epimorphism.

special_objects:
  initial object:
    description: trivial group
  terminal object:
    description: trivial group
  coproducts:
    description: direct sums
  products:
    description: direct products with pointwise operations

special_morphisms:
  isomorphisms:
    description: bijective homomorphisms
    reason: This characterization holds in every algebraic category.
  monomorphisms:
    description: injective homomorphisms
    reason: 'This holds in every finitary algebraic category: the forgetful functor to $\Set$ is faithful, hence reflects monomorphisms, and it is continuous (even representable), hence preserves monomorphisms.'
  epimorphisms:
    description: surjective homomorphisms
    reason: 'For the non-trivial direction, if $f : A \to B$ is an epimorphism, then $p \circ f = 0$ for the projection  $p : B \to B/f(A)$ implies that $p = 0$, so that $B = f(A)$.'
  regular monomorphisms:
    description: same as monomorphisms
    reason: This is because the category is mono-regular.
  regular epimorphisms:
    description: same as epimorphisms
    reason: This is because the category is epi-regular.