Timeline for W-types and inverse image functor
Current License: CC BY-SA 3.0
5 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Feb 19, 2023 at 14:22 | vote | accept | Aleš Bizjak | ||
| Feb 18, 2023 at 1:18 | answer | added | Ingo Blechschmidt | timeline score: 2 | |
| Sep 21, 2015 at 21:11 | comment | added | მამუკა ჯიბლაძე | 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. | |
| Sep 21, 2015 at 17:52 | comment | added | Andreas Blass | 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. | |
| Sep 21, 2015 at 16:22 | history | asked | Aleš Bizjak | CC BY-SA 3.0 |