# To what kind of generalized Lawvere theory does the “free cartesian closed category” 2-monad on $\mbox{Cat}_g$ correspond?

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?