I have moved the lead-in sentences out of the Definition-section into a new Idea-section (now here)

then expanded there a good bit, such as in making explicit the similarity to adjoint linear operators

and moved the Lawvere quote out of a footnote into a quote-environment

and added to it a paragraph quoted from p. 103 in MacLane71

]]>added a section “Transformation of adjoints” (here) with currently (just) the least general (but maybe most important) version of the definition (MacLane’s “conjugate” transformations) with a brief comment on the relation to bifibrations.

Since this probably deserves an entry of its own, I will also copy these paragraphs to a new entry *transformation of adjoints*.

Prodded by discussion here I have added to the very top of this entry highlighting of the parallel entry *adjunction*.

Yes, absolutely. We have some such referencing already, such as

but it could be developed much further.

]]>Sure, I can add that once the pull request gets merged.

In general it would be nice to systematically have links from nlab pages to their formalised equivalents in projects like the cubical library, the 1lab, and/or agda-unimath.

]]>Thanks. If there is a good/stable link to the Agda formalization, then let’s add it to the entry.

]]>Added composition of adjunctions (L’ ∘ L ⊣ R ∘ R’), precomposite adjunctions (— ∘ R ⊣ — ∘ L) and postcomposite adjunctions (L ∘ — ⊣ R ∘ —). Connected this to the fact that adjoints are absolute Kan extensions/lifts of the identity.

I couldn’t find this in the literature (but I didn’t look very hard), so if this is known under a different name, or if you have a reference, please add.

Formalisation of the pre/postcomposite adjunctions in Agda for the 1lab: https://github.com/plt-amy/1lab/pull/193/files#diff-b2e8196987b851f006e0efde215ecbf35f972e7eeee3ae3a1612cb4f8a480b61

]]>Mention that the comma category definition generalises to relative adjunctions.

]]>Yes, Instiki does not have markup for plain indentation. In fact, markup given by indenting by 6 or more whitespaces is interpreted differently altogether: it produces (indented, yes, but) verbatim output of the source.

]]>Huh. I’m surprised that indenting sections in the source doesn’t fix the “instiki gives up” issue. I guess this system works differently than others I’ve used. (or maybe I accidentally made a different error when trying this fix)

]]>Thanks, this is good material (here).

In the first lines I have fixed an “$L$” to “$F$” and an “$R$” to “$U$”, since that’s what you are using in the following. (On the other hand, myself, I prefer “$L \dashv R$” for the generic pair of adjoints, for what I find are obvious reasons: e.g. it is not generally the case that an

*U*nderlying functor is a right adjoint.)Then I took the liberty of removing the bullet item markup and replacing it by numeration by hand. This is a hack to workaround a shortcoming of the nLab software: Once you include

`tikzcd`

diagrams in an`Instiki`

bullet item, Instiki gives up and ends the itemize typesetting. As a result, the left alignment in your text did not come out as intended.(At some point in the future we are going to hire a programmer to fix this and related software issues.)

Added a proof that a pair of adjoint functors induces a monad.

]]>Yes, thanks for catching. Fixed now.

]]>Is there a typo in diagram (2) (the commutative square)? I don’t see how the vertical arrows are induced by $g:c_2\rightarrow c_1$ and $h:d_1\rightarrow d_2$ - I have read the definition of hom-functor. It works if $Hom(L(c_1), d_1$ is considered instead of $Hom(L(c_2), d_1)$, and same goes for other hom sets.

]]>Whoops! It was Prop. 1.9 that needed to have C and D switched. Done.

]]>Switched D and C in Prop. 1.10 to make it match the rest.

]]>Fix of the fix of the fix

]]>Fix of the typo fix…

]]>Fixed typos in diagrams.

]]>fixed typos

Spencer Dembner

]]>fixed typos

Spencer Dembner

]]>If you write `<https://edeany.com>`

it will automatically be a link (https://edeany.com).

Not clear what lemma you’re talking about. You should probably just state your lemma here rather than getting people to copy and paste your address into a separate window and then read a bunch of stuff.

]]>There is a certain lemma about adjoint functors that makes some of these things more manifest. See “Adjunctions” here https://edeany.com. Are people ok with me adding this lemma here?

]]>