Abstract: In the effective topos there exists a chain-complete distributive lattice with a monotone and progressive endomap which does not have a fixed point. Consequently, the Bourbaki-Witt theorem and Tarski’s fixed-point theorem for chain-complete lattices do not have constructive (topos-valid) proofs.
Download: fixed-points.pdf
Very nice paper!
I think there may be a typo in the first paragraph of Sect. 2, by the way: you define that X is discrete if the diagonal map X –> X^{\nabla 2} is _constant_. But if internally this is the condition that every map fron \nabla 2 to X is constant, i.e. in the image of the diagonal map, should the original condition be that the diagonal map is _epimorphic_?
Thank you for spotting that one. It should say that the diagonal map is an isomorphism, or equivalently epimorphism, as you suggest.