Quiver

[patrick-nicodemus]

In this PR, we

• Add a new constructor to Universal/Arrow.v so that one can more easily construct a universal arrow by appeal to its universal property. The definition of a Universal Arrow is in terms of comma categories and so contains the "dummy" category 1 and the functor 1 -> c; we give a constructor which omits reference to 1 and only talks about c.
• Added a new constructor for adjunctions in Universal/Arrow.v, so that one can construct a left adjoint to F: D ->C by proving that for every c in C, there is a universal arrow c -> F.
• In the file TList.v, we change the definition of a tlist so that one argument which was previously an annotation is now a parameter; this is a small change that should make proofs by induction slightly easier. We define a setoid equality on TLists where two paths are equal if they are the same length, if their nodes are strictly equal at each step in the path, and if their arrows are setoid equivalent at each step in the graph. (The existing setoid equality is only defined under the hypothesis that equality between nodes in the graph is decidable.)
• Added a new constructor to Theory/Adjunctions.v for an adjunction which does not require redundant data for the sake of duality.
• Added a new setoid structure for the type of functors C -> D, "strict equality", where two functors F, G are equal if F(c) = G(c) for all c, and if F(f) \cong G(f) for all f : c -> d. (This has been put in Theory/Functor.v after the other setoid structure.)
• Defined a new category, StrictCat, in Instance/StrictCat.v the category whose objects are categories, and whose morphisms are functors considered up to "strict equality."
• Defined a "quiver" in a new file Constructions/Free/Quiver.v. A quiver is a directed graph with a type of nodes and, for each node, a setoid of edges between them.
• We define the category of quivers and quiver homomorphisms.
• We define the "free category on a quiver", the category whose objects are the set of nodes of the quiver Q, and whose morphisms are formal paths through the edges of the graph. The identity morphism is the empty list, and composition of morphisms is given by formal path concatenation.
• We define the "underlying quiver" forgetful functor from StrictCat to Quiver, which sends each category to its underlying directed graph, and sends each functor to its underlying quiver homomorphism. Note that we had to use StrictCat rather than Cat in this definition, as the forgetful functor does not respect the equivalence relation of natural isomorphism which is asserted in the definition of Cat.
• For each Q, we construct a universal arrow from Q into the forgetful functor U : StrictCat -> Quiver, whose object part is the free category on Q. We use the aforementioned lemma on universal arrows to construct a left adjoint to U.

[patrick-nicodemus]

@jwiegley any interest?

[jwiegley]

I'm sorry to have been absent @patrick-nicodemus, yes I definitely have interest. Just looking for a chunk of time to review!

[jwiegley]

@patrick-nicodemus I'm very sorry this has taken so long. I'm going to incorporate your PRs as-is, and then afterward make whatever changes I think are needed to form it better to the overall design of the library — if such changes are even necessary at all!