A set is some elements. A map Blergs->Colors witnesses that each blerg b has a color fb in a manner that preserves equality.

A prequiver is a set of arrows, with a map to a set of sources and a map to a set of targets. For example, maps form a prequiver called Set.

A prequiver map is a map that preserves all equalities you can write in terms of the two maps and elements of the three sets. Prequiver maps form a prequiver Prequiv.

A quiver is a prequiver whose source and target sets are the same set of objects. Then we can ask whether the target of one arrow is the source of another. Quiv will preserve these equalities too. All prequivers so far were quivers.

A path in a quiver is n≥0 arrows between n+1 sources/targets. The paths in a quiver form a path quiver with the same object set. Pooossibly the definition of path can be made to fall out of the contrast between quivers and prequivers.

A compose-quiver is a quiver with a quiver map compose from its path quiver into it. Since they always share their object sets, I'll require compose to preserve every path's source and target.

There are several ways to take an arbitrary compose-quiver and redefine compose:

If the path has length one, return that arrow.
If the path has length four, conjure an arrow into its middle by composing the empty path corresponding to the middle object, then compose.
If the path has length three, compose the second arrow with the third, then compose the first arrow with the interim result.

I shall call these natural since they don't check objects for equality, as would allow removing any loops from the path before composing.

A category is a compose-quiver fixed by all natural redefinitions. Every quiver so far is a category.

A vector space evaluates linear combinations in an associative, unital manner. I could similarly have defined a category as a quiver with associative, unital compose. But the insight that led to what I was doing the last weeks was that this once, the above property also works. I suspect that this nails down all definitions on from prequiver.

A category map is a quiver map from one category's path quiver into another category that satisfies one of the following equivalent properties:

It is fixed by all natural redefinitions.
It preserves all equalities that can be written in a category's terms.

This forms the category Cat.

For example, there's a category map Cat->Quiv that forgets compose. In fact, it seems pretty unique.

A category map map (or natural transformation) between two category maps that share their source and target is a third which agrees on source-objects-of-output-arrows with the first category map and on target-objects-of-output-arrows with the second category map, with a property as above. This forms the category map category between two categories.

What follows is even less developed.

A semiquiver is a map with the connotation that its domain is arrowlike and its codomain is objectlike. A prequiver is two semiquivers that share their domain. A prequiver map is two semiquiver maps. A quiver map is not two semiquiver maps!

A prequiver map map between two prequiver maps is a third such that the first and third agree on sources and the second and third agree on targets.

Let's repeat everything so far in terms of itself. ...

Reflective category theory

Reflective category theory