Categories of graphs

[ScriptRaccoon]

This PR renames some existing categories of graphs, 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. 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.

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

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!), but as mentioned, the proofs are mostly using the language of relations. 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.

TODOS

• sets equipped with a reflexive relation ("reflexive directed graphs")
• sets equipped with a reflexive symmetric relation ("reflexive undirected graphs")
• sets equipped with a symmetric relation ("undirected loop graphs")
• sets equipped with an equivalence relation (maybe in another PR)