The proof Michael Barr had in mind at the time of writing his 1986 JPAA paper on representations of categories, and has now clarified, is truly beautiful. I may have misrepresented what the problem was with presenting the transfinite induction part of the proof in my course. It is a question of time rather than difficulty. I am not known amongst my colleagues as one who shrinks from teaching or avoiding hard proofs. The point is that I have a course consisting of 24 lectures to a group including a (bright) 4th year student (who had hardly heard of categories before the course), a graduate students in number theory, physics and computer science, my own 5 PhD students, and a professional category theorist. I am trying to keep it interesting for all. The students (even the ones who have done a formal set-theory course) have not really used ordinals; so I would need to sacrifice some category theory to provide that background. I am still undecided about this; perhaps, the transfinite induction and the embedding theorem can be an appendix to the course. Perhaps the most novel aspect of the course, considering my 2-cell background, is that I have given 18 lectures so far without introducing natural transformations. I'm about to talk about adjunctions without them too. I must admit that the course content has evolved on the run. But looking back, I think it has some unity of purpose. I headed straight for the definition of regular category as having a terminal object, pullbacks, strong epi - monic factorizations, and stability of strong epis under pulling back along arbitrary arrows. We developed the method of generalised elements and constructed the Poset-enriched category of relations in a regular category. We proved relations with right adjoints are graphs of arrows. We proved strong epis are regular. Equivalence relations and (Barr-)exact categories were examined. [One of my (intended?) questions to Michael Barr was whether he knew of a diagram lemma which could be proved significantly quicker using the embedding theorem than by the generalised-element/relations technology.] I proved in detail that an exact additive category is abelian (as defined in Freyd's book "Abelian Categories" - beginning of Chapter 2). Not only is that a deep theorem of category theory (in my opinion - despite not needing a transfinite argument) but it is a microcosm of categorical ideas that have proved useful in other contexts. We proved the Five Lemma, Snake Lemma using relations in the abelian category. So far I have set 15 exercises: some quite challenging. One was to prove Cat is not regular (I gave a bit of a hint). Now I am discussing 2-sided discrete fibrations (just for categories) in depth. These are being advertised as the "relations" of category theory. In fact, this means we do have presheaf categories disguised as DFib(A,1); so some natural transformations are there hiding there. I have this weekend to decide where we go next! But I think there is enough meat in all this to deal with sceptical colleagues. When it comes to a game of "my subject's harder than yours, nya, nya", I would also argue that the concepts category theory has to offer are just as hard to really master as difficult theorems. This is why many mathematicians calculate hard to do what we can do with our concepts. Regards, Ross