In a message with [Subject: A diagram lemma] Mike Barr asks:
Has anyone seen the following diagrammatic lemma?
Sure -- in the general case. Remember the business about "lim-pacing" functors in Lawvere's Columbia PhD thesis? A functor C ---> D is lim-pacing iff: for every diagram, anywhere, of shape D , if the "restricted" diagram of shape C has a limit, then so does the original one, and the canonical "comparison" between those two limits is an isomorphism. There are n.a.s.c.'s internal to C and D for the lim-pacing condition (some comma category being non-empty and connected); and your "diagrammatic lemma" is just the instance of all these obtained with C = NNO^op and D = (NNO x NNO)^op (and C ---> D the diagonal). [No one would probably want to bother promoting this particular case to the status of a "lemma".] Hope this helps. -- Fred ==================================