Ah, thanks!

]]>I put in a little more detail about when B-W holds, namely in any topos with a geometric morphism to $Set$, together with a reference to the Bauer-Lmsdaine paper where this is proved, and which Peter linked to in the n-Café discussion.

For reference, and for perhaps sorting out later, there seems to be two versions of Andrej’s paper: in the Proceedings of the 25th Conference on Mathematical Foundations of Programming Semantics (MFPS 2009) proceedings in Electronic Notes in Theoretical Computer Science in 2009 and in the Mathematical Foundations of Programming Semantics (MFPS XXV) proceedings in Theoretical Computer Science in 2012. The papers are different lengths, so I don’t know what is going on.

]]>Coming back to Zorn’s lemma, I found that its proof from AC (which was mainly my doing) was inadequate, so I fixed it up. If anyone knows where such a proof appears in the literature, I’d like to hear it. I thought when I first wrote it up here a few years ago, I had gotten it from Lang’s Algebra, but checking this now it looks rather different, and now I have no idea where it originally came from.

I also wrote up some stuff there on the Bourbaki-Witt fixed point theorem, this time following Lang for sure.

]]>I found the organization at *Zorn’s lemma* a bit rough, so I have tried to smoothen it out a bit

For instance

at one point it had suddenly said “proof of the converse” without a clear statement of the other direction having appeared before. I have created two Theorem-environments and tried to make the statements clearer.

the Idea-section had started out saying that “Zorn’s lemma is a trick”. I think that’s misleading or at least misses the important nature of the thing, so I rewrote that and expanded a bit.

But the foundationalists among you please check!

]]>