The Coq mailing list

[Andrej Bauer <andrej.bauer AT andrej.com>]

> (Martin Escardo and Paul Taylor tell me that Dito Pataraia showed that
> this fixed point theorem also holds in intuitionistic set theory, but
> to my knowledge there isn't a predicative version of it.)

Yes, and Pataria's proof is hard to find. A proof is available in
http://dis.ijs.si/France/notes/join-induction.pdf (Corollary 9), and a
quick outline in http://arxiv.org/pdf/1201.0340.pdf (Theorem 3.2).

With kind regards,

Andrej