All sheaf topoi have W-types and in fact there's an explicit construction given by Benno van den Berg & Ieke Moerdijk, but the construction is quite involved.

I would like to know whether the inverse image part of a geometric morphism always preserves W-types for more general reasons or pointers to references detailing the conditions on functors so they preserve W-types.

Inverse image functors always preserve the natural numbers object, which is a particular kind of W-type, but the proof of this fact is very specific to the NNO so this might suggest that they don't all preserve W-types, but I have not found anything about this stated anywhere.

  • 1
    $\begingroup$ I don't know enough about the details of W-types, but I conjecture that an old paper of mine might be useful: Well-ordering and induction in intuitionistic logic and topoi, in "Mathematical Logic and Theoretical Computer Science" (D. W. Kueker, E. G. K. Lopez-Escobar, and C. H. Smith, eds.) Marcel Dekker, Lecture Notes in Pure and Applied Mathematics 106 (1987) 22--48. One of the results in that paper is that inverse-image functors of topoi preserve totality of inductive constructions, which seems closely related to W-types. $\endgroup$ Sep 21 '15 at 17:52
  • 3
    $\begingroup$ Presumably you at least need to require that the the inverse image functor respects the dependent product involved in the definition of the W-type. For finitary ones (that is, for initial algebras of endofunctors which are polynomial in the most restrictive sense, $A_0+A_1\times X+A_2\times X^2+...+A_{42}\times X^{42}$ say) or something slightly more general defined through NNO there should be no problem and it should work, but for more general W-types - I doubt it without additional requirements. $\endgroup$ Sep 21 '15 at 21:11

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.