Re: two questions about universal quantification

Barry Jay asked

Has the following lemma been seen before?

Lemma: If D is a cartesian closed category having all finite limits then so is its arrow category.

This is a special case of the cartesian closedness of a category obtained by Artin glueing, which was covered in the Carboni--Johnstone paper (Math. Struct. Comp. Sci. 5 (1995), 441--459). (However, we don't claim any originality for it; it is implicit in Gavin Wraith's 1974 paper on Artin glueing.) Of course, the "glueing functor" in Barry's case is the identity on D. Peter Johnstone