Oh, silly me, I should have announced: no, choice principles are not required!

Now that I've stared at this reference a bit longer, I can see it definitely answers my question. This is a very elegant development (which I'll probably write up on my personal web at the nLab, for possible exportation to the nLab proper), and I thank you again Andrej for bringing it to my attention.

This looks like it probably answers my question (and then some!), but I'll need to look it over more carefully when I find some time. Thank you!

Thanks Emerton -- I was sort of aware of this, but the comment surely deserves to be made.

As usual, you are very helpful, Mike -- these look like very nice leads! I'll take a look at the Elephant. Someone somewhere else also suggested I consider nets/filters, so this angle is probably worth another look as well.

No conditions are put on $Y$. As you observe, the a priori weaker implication we get by strengthening the hypothesis to say (e.g.) "if $Y$ is compact Hausdorff" is nevertheless sufficient to prove compactness, at least if choice is assumed.

Maybe not everyone, researchers included, is sufficiently familiar with just-do-it proofs? Link: tricki.org/article/Just-do-it_proofs

Perhaps a side issue, but I don't understand what you mean by pseudofunctor here. To me, a pseudofunctor is a type of map between 2-category or bicategory structures, but I am not aware of any interesting 2-category structure on the category of PL manifolds.

I am not familiar with this notion of exact category (and my gut feeling is that it isn't a very useful notion, although I would welcome being shown otherwise). But is the category of pointed compactly generated Hausdorff spaces an example? What if you take $f$ to be the identity function from the real line with the discrete topology to the real line with its standard topology?

Sorry to have to eat my words, Mark. I appreciate the time you put into this, and I wish I could accept your answer as well. But Derek Holt's solution was a bit easier for me to follow.

Wow, this is a really great example; it gives everything I was asking for. Thanks very much!

Well, I surely believe that you get the desired relations if $x$ and $y$ are algebraically independent, but Mark's objection would still need to be addressed.