Dear Fellow Categorists: I am personally not likely to take up Harvey Friedman's challenge, having long been doing "category theory as algebra" rather than "category theory as foundations". I would like to point out, though that Friedman has deliberately chosen as a test case real analysis, a subject which exists only to simulate the existence of fluxions on the basis of foundations tied to two-valued logic. How about asking Friedman to give an elegant, elementary foundation for rings satisfying the Kock-Lawvere axioms? The use of an axiom schema in which arbitrarily complex formulae may be subsituted also seems a bit of a dodge. At first glance, elementary topoi plus NNO, well-pointed and choice still doesn't need such things (but I could be wrong, not having thought much about it for years). Best Thoughts, David Yetter