Thinking of Cat as a mere 1-category, there is a 1-monad $\Lambda$ for the free cartesian closed category on a category. To every category X it assigns the category $\Lambda(X)$ whose objects are generated by $\times, \multimap, 1,$ and the objects of $X.$ (I'm using $\multimap$ instead of the usual $\to$ to avoid collisions with the arrows for morphisms and 2-morphisms.) Its morphisms are generated similarly, but given $f\colon x\to y$ and $f'\colon x' \to y'$, we get the morphism $$f\multimap f'\colon (y \multimap x') \to (x \multimap y').$$

The monad $\Lambda$ does not extend to a 2-monad because of the contravariance of the first slot of $\multimap$: suppose we have functors $x, y\colon 1 \to X$ that pick out objects $x, y$ from the category $X$, and a natural transformation $f\colon x \Rightarrow y$ between them. Then $\Lambda(1)$ is the free cartesian category on one object $\bullet$; $\Lambda(x)$ is the functor that replaces each copy of $\bullet$ in a formula like $\bullet \multimap \bullet$ with the object $x$, and similarly for $\Lambda(y)$; and $\Lambda(f)$ should be a natural transformation between them that assigns to each object like $\bullet \multimap \bullet$ in $\Lambda(1)$ a morphism

$$f\multimap f\colon x \multimap x \to y \multimap y$$

in $\Lambda(X).$ Such a morphism doesn't exist, in general, but does if $f$ is an isomorphism; so $\Lambda$ is 2-monadic over $\mbox{Cat}_g,$ the category of small categories, functors, and natural isomorphisms.

Finitary monads over Set correspond to Lawvere theories. Power showed that when a symmetric monoidal biclosed category $V$ has finite cotensors, finitary $V$-monads correspond to $V$-enriched Lawvere theories. We set $V = \mbox{Cat}_g$.

$\Lambda$ looks finitary, in that any formula is finite, but it looks like a $\mbox{Cat}_g$-enriched Lawvere theory doesn't have the ability to talk about opposites of objects. Is there some notion of generalized Lawvere theory that does?


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.