Hello, I think that following preprint might be of interest to some people on the list: Title: Internal Diagrams in Category Theory Abstract: We can regard operations that discard information, like specializing to a particular case or dropping the intermediate steps of a proof, as _projections_, and operations that reconstruct information as _liftings_. By working with several projections in parallel we can make sense of statements like "$\Set$ is the archetypal Cartesian Closed Category", which means that proofs about CCCs can be done in the "archetypal language" and then lifted to proofs in the general setting. The method works even when our archetypal language is diagrammatical, has potential ambiguities, is not completely formalized, and does not have semantics for all terms. We illustrate the method with an example from hyperdoctrines and another from synthetic differential geometry. It is at: http://angg.twu.net/LATEX/2010diags.pdf Best wishes to all, Eduardo Ochs eduardoochs@gmail.com http://angg.twu.net/ [For admin and other information see: http://www.mta.ca/~cat-dist/ ]