@John
> By the way, Keith, you're writing \$$g \circ h\$$ to mean "do first \$$g\$$ and then \$$h\$$", while most category theorists - and in particular me - use it to mean "do first \$$h\$$ and then \$$g\$$", just as we do for functions, where
>
> $(g \circ h) (x) = g(h(x)) .$

So... I have been trying to write up how to use Lawvere's fixed point theorem to prove Gödel's second incompleteness theorem as per our discussion.

In [Lawvere's 1969](http://tac.mta.ca/tac/reprints/articles/15/tr15.pdf) paper I think he used the opposite convention for composition :

> Taking the case \$$X = 1\$$, one has that every \$$f : A \to Y\$$ gives rise to a
unique \$$\ulcorner f \urcorner : 1\to Y^A\$$ and that every \$$1 \to Y^A\$$ is of that form for a unique \$$f\$$.
> Since for every \$$a : 1\to A\$$ one has (dropping the indices \$$A\$$, \$$Y\$$ on \$$\epsilon\$$ when they are clear)
> \$\langle a, \ulcorner f\urcorner \rangle = a.f \$
> one calls the “evaluation” natural transformation; note however that we do not assume
> in general that \$$f\$$ is determined by the knowledge of all its “values” \$$a.f\$$

(the above is from page 4)

It's confusing!