A vaguely working categories library. Much to do still...
Subsuming A-K-S.

Ahrens-Kapulkin-Shulman 1-categories are subsumed in our notion of
concrete 2-category.

It turned out to be surprisingly painless to prove, which is good
evidence we're on the right track.