Beefing up adjunctions.

[anuyts]

Generalize/factor definition of adjunction (as natural bijection) to include ad hoc (per-object) and relative adjoints.

[anuyts]

Copying from a comment in the code:

Here, we define adjunctions in terms of more general concepts:

• Relative adjunctions (see e.g. the nLab)
• Adhoc adjunctions: Sometimes a functor F does not have a right adjoint functor G defined on all objects, but for a specific object d, there may be an object gd that behaves as the image of d under the right adjoint to F. Examples are:
  • the local right Kan extension (when the global Kan extension does not exist)
  • a limit of a specific diagram (when not all diagrams of the same shape may have a limit).

[anuyts]

I would very much welcome suggestions on how to better hide the increased generality for users only interested in ordinary adjunctions.

[felixwellen]

I would very much welcome suggestions on how to better hide the increased generality for users only interested in ordinary adjunctions.

How about splitting it up into two files, RelativeAdjunction.agda and Adjunction.agda? - Where The latter imports the former.

[anuyts]

Is that a good programming pattern? It would mean that an adjunction relative over the identity functor is not an adjunction.

Remarks on this particular case:

• I think the inclusion of relative adjunctions rarely actually gets in the way of users of ordinary adjunctions, given the excellent computational behaviour of the identity functor,
• Actually, my primary goal was to include ad hoc adjunctions like local Kan extensions, and it seemed unpractical if these would be defined not in relation to proper adjunctions. In a way, this seems undisturbing as well: the proof obligations remain exactly the same.
• The thing that bothers me most is that the names isLeftRelativeRightAdhocAdjunction and isLeftAdhocRightRelativeAdjunction will pop up when people are dealing with non-relative non-adhoc adjunctions. I'll see what I can do about that.

On a higher level, since Cubical.Categories is a category library, and since in category theory pretty much everything is a special case of something else, we should think about a principled approach for dealing with that.

[anuyts]

Currently, I think that content-wise my current definition of ordinary adjunctions aligns pretty well with the original one, and should support a fair extent of backwards compatibility. However, I ran into issues with Agda's module system:

• Overlapping but consistent imports of the same definition under the same name cannot be used, so that open imports are generally a bad idea, so that you generally have to import a module as well as all its dependencies, agda/agda#6035
• agda/agda#6004
• open statements cannot take arguments, so a (non-public) open with an argument has to be encoded as a nameless (private) module containing a public open, agda/agda#6036
• even though there is a separate module X to Y syntax for renaming modules, the ordinary X to Y syntax seems to affect modules as well. agda/agda#6037

As a result, I get significant opening boilerplate in the section "Proofs of equivalence" in Cubical.Categories.Adjoint.

When I have more time, I will create issues for these matters / clarify the one that I have already created. (Done.)

[anuyts]

@jacquescarette pointed out this paper in relation to the sort of problems we're facing here, though I haven't yet distilled what we should learn from it.

[anuyts]

Quoting @maxsnew:

I think if we want a "most general" version of a universal property, a good one to pick in my experience is "representable profunctor", i.e. a profunctor C^o x D -> Set that is equivalent to a composition of Hom with a functor either from C to D or vice-versa. This includes adjoint functors, relative adjoint functors, limits, colimits, Kan extensions etc very directly. I hacked something up here that could be cleaned up and submitted (https://github.com/maxsnew/cubical-cbpv/blob/main/Profunctor.agda).

Yes, I considered going this far but I was afraid it would be too alienating to most users interested in the more well-known instances you're listing.

[felixwellen]

I think alienation is not a problem, if you just provide an example everyone knows. Without too much thought, I can imagine the following to be a good way set things up:

• Put it in Cubical.Categories.UniversalProperty.Base (maybe just an import)
• Make a module Cubical.Categories.UniversalProperty.Example, where a universal property everyone knows is instantiated
• Add something to the example everyone wants to do, i.e. show that something having a universal property, is determined up to unique iso.

Disclaimer: I don't know my way around the categories-part of the library, so maybe that's already done somewhere else, for a different notion of universal property.

[anuyts]

I guess a fully representable functor can be used to show that a thing with a universal property always exists, e.g.

• all limits of diagrams of a given shape exist,
• a global Kan extension exists,
• an adjoint functor exists.

I think I still need the ad hoc variant for individual instances:

• one given diagram has a limit,
• a local Kan extension exists.

But yes, if there's a consensus among the few people who are around here that deriving simple concepts from more general concepts is a good library development pattern, then I might commit something along these lines (perhaps after reading Jacques Carette's paper).

[JacquesCarette]

My opinion on "good library development patterns":

• the interface to a structure should look 'familiar'. This is why we don't use duality to define dual concepts -- otherwise the cognitive burden on users is too high.
• the proof of any given result is allowed to use whatever machinery seems good. So specializing high-powered proofs is completely legitimate here.

The basic difference is between users, for whom we want the bar to be low, and library developers, whose overall workload we want to minimize. What gets squeezed in the middle is the 'user' who wishes to use a library to learn things... they might be forced to learn a lot more than they intended if they're trying to understand the proofs.

[maxsnew]

I think I still need the ad hoc variant for individual instances:

One of the nice things about representables is that they subsume these cases as well.

I.e., a category C has all products when the profunctor ((C x C)^o x C -> Set)

((a,b),c) |-> C(a,c) x C(b, c)

Is representable, and to say a particular pair of objects a,b in C has a product is to say that the profunctor (1^o x C -> Set)

(*, c) |-> C(a, c) x C(b, c)

is representable.

[maxsnew]

And I agree with Felix's plan. More concretely, we can define representable profunctor in some module and prove some "Yoneda facts":

1. It determines a functor up to unique natural iso
2. The representability is determined by a universal morphism

Then for particular UMPs we would define their own module with a "pedestrian" definition, and a "slick" definition using representability and prove they are equivalent. In my experience the pedestrian definition is just explicitly describing the universal morphism so this might not be as hard as it sounds. We can then transport general proofs about representables to the pedestrian formulation.

[anuyts]

One of the nice things about representables is that they subsume these cases as well.

Well ok but it seems more useful to define a representable profunctor as one that has an ad hoc representation for every object, ~naturally~ functorially, than to define an ad hoc representation as a degenerate case of a representable profunctor, including a vacuous ~naturality condition~ functorial action.

In a specific case: it is more useful to define a global Kan extension as a local Kan extension everywhere, ~naturally~ functorially, than to define a local Kan extension by a not very similar looking universal property.

Or: it is more useful to define having all limits of a given shape as having a limit for every diagram, ~naturally~ functorially (hmm, is this ~naturality~ functoriality automatic? I believe so.) than to define having one limit as a fairly unrelated concept.

What does UMP stand for?

[plt-amy]

"universal mapping property" (quick edit: I haven't reviewed the PR so don't have anything useful to say on its contents, but I saw the question on discord)

[maxsnew]

@anuyts

You can show that for a fixed profunctor R : C^o x D -> Set that the following are equivalent:

1. A functor F : C -> D and a natural iso D(F(c), d) =~ R(c, d)
2. A function on objects F_0 : C_0 -> D_0, and a family of “universal elements” R(c, F(c)) such that composition with universal elements produces an (automatically natural) isomorphism D(F_0(c), d) =~ R(c, d)

And since a profunctor is the same as a functor R : D -> Psh(C), by (2) above this reduces representable profunctors to being point-wise representable presheaves. So you can use either as the basic notion, it's a matter of taste. I simply prefer representable profunctors because they generalize to arbitrary pro-arrow equipments, which is the setting I'm most familiar with and generalizes to enriched/indexed category theory where presheaf categories don't necessarily exist. But I admit that's not a strong argument for preferring them to representable presheaves as the basic notion in this library.

Edit: remove the naturality constraint which as @anuyts points out doesn’t make sense

[anuyts]

Oh right, I actually proved 2 => 1 in the current pull request (the module RightFunctoriality). To be entirely precise about 2: You can't state that the element of R(c, F(c)) is natural if F isn't functorial yet, but you can construct the functorial action from the isomorphism D(F_0(c), d) =~ R(c, d) and then the naturality is provable.

[felixwellen]

@anuyts: Is this intentionally left in draft state?

[anuyts]

@felixwellen Yes, I'll consider what to do with this later.