and a strict 2-adjunction is analogous, where are instead strict 2-categories, are strict 2-functors, and is a strictly 2-natural isomorphism of hom-categories. A lax 2-adjunction is given by a (suitably natural) pair of functors
such that .
Just as the notion of adjunction makes sense not just in but in any 2-category, lax 2-adjunctions can be defined in any 3-category when the above is suitably reformulated by using the 2-categorical Yoneda lemma. So, given 0-cells and 1-cells , in any 3-category, we say is lax left adjoint to if we have
2-cells and , and
instead of strict triangle equalities, 3-cells (called triangulators)
satisfying the swallowtail identities:
Mike: What 3-category are we intended to work in to obtain an equivalence with the original notion? I guess this is the question of how strict we require to be and whether “suitably natural” means “strictly 2-natural” or “pseudo natural.”
Since on the nLab, everything is weak by default, it seems that we should probably use the unadorned name for the version where , are weak 2-categories, and are weak 2-functors, and and are pseudo natural.
Finn: For Gray, are all strict, and are lax. I’m still trying to understand the connection between the two formulations, so I’m not sure how extra weakness on one side translates to the other. I should have a better idea soon.
Mike: Unfortunately, there is no 3-category, not as usually understood, in which the 2-cells are lax transformations. The interchange law for whiskering lax transformations holds only laxly, so at most you have some sort of ‘lax 3-category.’ Actually, in the case of , what you have is that with the lax Gray tensor product is biclosed and hence enriched over itself, and that sort of enrichment is the relevant 3-category-like structure. (More grist for my mill that lax things are important!)
Finn: Yes, that’s been worrying me. Figuring out the relationship between the two definitions will be my mini-project for the coming week – it’s about time I got to grips with this sort of enriched-Yoneda wizardry.
Gray shows that given a strict 2-adjunction between the 2-comma categories and you get lax . Maybe using a stricter comma construction will yield pseudo-natural unit and counit – I don’t know, but I’ll try to find out. (Of course, any hints or suggestions you have will be greatly appreciated!)
Mike: One thing worth pointing out is that there is no Yoneda lemma for lax transformations (though there is for pseudo ones). So in order for to be determined by , must be pseudo natural in , and likewise for to be determined by , it must be pseudo natural in . My guess is that laxity in the remaining variable will correspond to laxity of and , and will come from the adjunction . That suggests that if we do everything in a (strict or weak) 3-category, so that and must be at least pseudo, we get the homwise notion where “suitably natural” means strict or pseudo.
It appears that in Seely’s paper (referenced below) the functor , at least, is also lax. Lax functors are even harder to incorporate in a 3-category-like structure than lax transformations are; you can’t even whisker any sort of transformation by a lax functor. Moreover, he also seems to say that and are both strict in their first coordinate, rather than one in the first and one in the second as seems (to me) to be necessary for a Yoneda restatement. Hmm.
This idea was introduced in Gray’s book under the name of transcendental quasi-adjunction.
Mike: Is there a reference for the name “lax 2-adjunction?” It looks very similar to the notion of “local adjunction” in
except that they allow to be an oplax functor, a lax functor, an oplax transformation, and a lax transformation.
Mike: Kelly-Street don’t say anything about lax adjunctions. I want to make sure we think seriously about what this sort of thing should be called, rather than just following one or another author. As far as I can tell, it doesn’t fit into the general precise meaning of ‘lax’ (being a type of morphism of algebras for a 2-monad), and there are so many possible variations (as in Gray’s book) that it might be nice to have a sensible system of nomenclature that would include them all. Maybe. On the other hand, I actually never really took Gray’s stuff very seriously because I couldn’t think of any examples; maybe I should look more closely at Seely’s paper.
Finn: Yes, that would be nice, but I for one don’t know enough yet about the big picture to make any suggestions that would generalize easily.
I’m interested in this stuff because I want to use strict 2-categories with lax structure to model rewrite systems, as Seely does. These lax/quasi/local adjunctions are one way of specifying lax structure, but there are probably others (3-monads on 2-Cat? Lawvere 3-theories?).
Mike: I don’t understand how Seely’s definitions give you a 2-category; all I can see is a ‘lax 2-category’ of some sort. If the composite of lambda terms and is defined by , then we have
which are (as far as I can tell) not the same, but both admit a beta reduction to . Is there some other way of defining composition so that it is associative?
Finn: The composite is defined to be the substitution of for the free variable of . Associativity follows. Substitution is meta-notation, and not part of the syntax of -calculus.
If and (where is application and is a fresh variable), then the ‘local’ adjunctions give
which when combined with the definition of composition as substitution give you exactly the -reduction and -expansion laws.
Mike: Ah, I didn’t notice that the morphisms from to are terms of type with a free variable of type , rather than the (to me) more obvious choice of terms of type . I don’t follow your second paragraph, though.
(Of course, on a moment’s reflection that choice makes perfect sense; those are the same as the morphisms in any other category of contexts.)
Finn: Right – it’s the usual functorial semantics interpretation: composition is substitution.
The second paragraph was just pointing out an example of how a lax adjunction arises in typed -calculus. You want types to map to 0-cells and terms to 1-cells as usual, and rewrite relations to map to 2-cells . So the term model will be a strict 2-category with (strict or lax) products, together with lax left adjoint to for all . Then the first definition of lax adjunction should give you the and rewrites as the counit and unit of each adjunction . As I’ve said above, I’m still working out the details wrt pseudo versus lax naturality, but this is roughly what you should get.