Various people (including Moerdijk & Palmgren, Hyland & Gambino, Abbott & Altenkirch & Ghani) have considered locally cartesian closed pretoposes with W-types, ie initial algebras for generalized polynomial functors, aka 'containers'. (These W-types are an appropriate analysis of the fixed points of intensional constructions and so these categories have been motivated as "constructive toposes", as models of a particular version of Martin-Lof's type theory). Lcc pretoposes are Heyting pretoposes. For any object X, consider those monotone endofunctions on the class Sub(X) that can be constructed from the pullback functors and their left and right adjoints. By my calculations, in a topos, these monotone endofunctions have least and greatest fixed points (by internalizing them and then using Tarski's fixed point theorem). It seems that, in general, these monotone endofunctions will not have least or greatest fixed points in lcc pretoposes with W-types. (I haven't proved this, though, and perhaps I have missed a neat trick.) If I'm not mistaken, this is a mismatch. Lcc pretoposes let you work both intensionally and extensionally, yet when it comes to W-types, we only consider the intensional constructions. Is there a reason for this?-- are these fixed points "non-constructive" or "impredicative" in some sense? Has anybody thought about these things before? Have I missed something? All the best, Sam [My example is bisimilarity for transition systems, as studied in concurrency theory. This is conventionally calculated as a maximum fixed point for a monotone endofunction on the lattice of binary relations. I can define a 'constructive' version of bisimilarity using W-types, and then take the image. This differs from the usual notion, unless choice is assumed.]