theorem about ends

Dear all, Does the following result (which I learnt from Rasmus Mogelberg) appear in the literature somewhere? Given categories C and D, a functor P : C^op x D --> Set and an adjunction F -| U : D --> C the end over c in C of P(c,Fc) is (isomorphic to) the end over d in D of P(Ud,d). Paul -- Paul Blain Levy School of Computer Science, University of Birmingham +44 (0)121 414 4792 http://www.cs.bham.ac.uk/~pbl [For admin and other information see: http://www.mta.ca/~cat-dist/ ]