[ScriptRaccoon]

This PR renames two existing categories of graph-like structures, improves the associated terminology, and adds several new ones.

Renamings

The category DiGraph (from #372) is renamed to Quiv, and accodingly, directed graphs are renamed to quivers, aka directed pseudographs. This is much more precise and also a prerequisite for adding more special categories of graphs.

In other words, directed graphs are not allowed to have multiple edges (but they may have loops). The description of Bin (from #372) has been changed accordingly. Its objects may be identified with directed graphs.

Conventions

Unfortunately, graph theory has lots of different conventions even for the most basic notions: The term "directed graph" usually allows loops, but the term "graph" usually does not, namely when it refers to "undirected graph", but every book does it differently; category theorists even tend to write "directed graph" for "quiver"; the term "simple graph" has no agreed-upon definition; many graph theorists assume graphs to be finite and/or non-empty, etc. See also nLab.

To prevent any confusion, the categories of graphs introduced in this PR are focussing on their specific models: sets equipped with a relation of a specific type. For example, the objects of Bin are not primarily interpreted as directed graphs. They are just pairs (X,R), where X is a set and R is a binary relation on X. The proofs of the categorical properties are actually much simpler in this language.

To highlight the graph-theoretic interpretations, though, structures now support an alternative_notation field. For example, DiGraph is an alternative notation for Bin, and Graph is an alternative notation for Bin_symm,irr. It is displayed in the summary on the structure detail page.

Sets equipped with an irreflexive binary relation ("directed graphs without loops")

This PR adds the category of sets equipped with an irreflexive binary relation. These model directed graphs without loops, but as mentioned, the proofs are mostly using the language of relations. All properties have been decided.

Even though this was not the initial objective, this category witnesses lots of new combinations, thus contributing to this milestone. The number of missing combinations is now 293.

Found 28 unique witnessed combinations by the supplied structures (Bin_irr):

Directly witnessed:
- countably extensive ∧ ¬filtered
- countably extensive ∧ ¬ℵ₁-filtered
- directed colimits ∧ ¬quotients of congruences
- filtered colimits ∧ ¬quotients of congruences
- filtered-colimit-stable monomorphisms ∧ ¬quotients of congruences
- finitely accessible ∧ ¬quotients of congruences
- finitely accessible ∧ ¬reflexive coequalizers
- finitely accessible ∧ ¬sifted colimits
- infinitary extensive ∧ ¬filtered
- infinitary extensive ∧ ¬ℵ₁-filtered
- locally cartesian closed ∧ ¬quotients of congruences
- locally finitely multi-presentable ∧ ¬quotients of congruences
- locally finitely multi-presentable ∧ ¬reflexive coequalizers
- locally finitely multi-presentable ∧ ¬sifted colimits
- locally multi-presentable ∧ ¬quotients of congruences
- locally multi-presentable ∧ ¬reflexive coequalizers
- locally poly-presentable ∧ ¬quotients of congruences
- locally poly-presentable ∧ ¬reflexive coequalizers
- sequential colimits ∧ ¬quotients of congruences

Dually witnessed:
- countably coextensive ∧ ¬cofiltered
- countably coextensive ∧ ¬ℵ₁-cofiltered
- directed limits ∧ ¬coquotients of cocongruences
- cofiltered limits ∧ ¬coquotients of cocongruences
- cofiltered-limit-stable epimorphisms ∧ ¬coquotients of cocongruences
- infinitary coextensive ∧ ¬cofiltered
- infinitary coextensive ∧ ¬ℵ₁-cofiltered
- locally cocartesian coclosed ∧ ¬coquotients of cocongruences
- sequential limits ∧ ¬coquotients of cocongruences

Note. After adding the category below, the command for the single category will not show these results anymore. Use both then.

pnpm db:combinations category Bin_irr Bin_symm_irr

Sets equipped with a symmetric irreflexive binary relation ("undirected graphs")

This PR adds the category of sets equipped with a symmetric irreflexive binary relation. These model undirected graphs (where loops are not allowed, which seems to be more common in the literature, the opposite as for directed graphs!). All properties have been decided.

Actually, the (currently recorded) properties are exactly the same as for the irreflexive relations, and the proofs are very similar. In a comment I give a proof why the categories are not equivalent.

Sets equipped with a reflexive binary relation ("reflexive directed graphs")

This PR adds the category of sets equipped with a reflexive binary relation. These model reflexive directed graphs (i.e. where each vertex has a loop). It turns out that there are not so many differences to Bin. No new combinations are witnessed.

Sets equipped with a symmetric binary relation ("undirected loop-graphs")

This PR adds the category of sets equipped with a symmetric binary relation. These model undirected loop-graphs. All properties have been decided.

Actually, the (currently recorded) properties are exactly the same as for all relations, and the proofs are very similar. In a comment I give a proof why the categories are not equivalent.

Sets equipped with a symmetric reflexive binary relation ("reflexive undirected graphs")

This PR adds the category of sets equipped with a symmetric reflexive binary relation. These model reflexive undirected graphs. All properties have been decided.

Actually, the (currently recorded) properties are exactly the same as for reflexive relations, and the proofs are very similar. In a comment I give a proof why the categories are not equivalent.