Define adjunctions

[mikeshulman]

There are a lot of choices as to how to go about that, each of which has different possible amounts of coherence:

• Equivalences of hom-functors
• Unit and counit with triangle identities
• Comma categories and universal arrows

To what extent are they equivalent? Which one(s) should we use?

[mikeshulman]

Comma categories and universal arrows appears to be the only "fully coherent" one, so maybe we should start with that. Depends on #35 .

[Alizter]

OK, I have managed to "write down" definitions of having a left and right adjoint. These can be found in WildCat/Adjoint.v. The only issue is that our IsInitial relies on there being 2-cells in a category, which means we have to have the comma category be a 1-cat. Comma categories are only 1-cats if at least the B in A -> B <- C is a (2,1)-cat which means we can only talk about left adjoints of 1-functors into (2,1)-cats. This doesn't seem like an ideal way to go about things.

The solution to this is to have some hierarchy for the structure of a 1-cat. Saying stuff like a wild cat with 2-cells but no coherences for them etc.

This is why I actually managed to write down a definition of "having a left adjoint" for ooCat.v before our regular wild cat stuff.

[mikeshulman]

The solution to this is to have some hierarchy for the structure of a 1-cat.

... or, perhaps, to use oo-categories everywhere!