Lutz Schroeder asked:
is there a good reference for the construction of inductive datatypes (lists, trees etc.) in a topos with nno (assuming that my guess that such a construction is indeed possible is correct)?
Thomas Streicher replied:
It is not clear to me to which extent one can characterise those inductive types that can be reduced to inductively defined predicates in HAH. However, one knows that assuming W-types (`a la Martin-Loef) one can reduce most inductive types to W-types in extensional type theory. As far as I understand that's the reason why Moerdijk and Palmgren introduced lccc's with W-types as sort of ``predicative toposes''.
Just to point out that "assuming W-types" here is no extra assumption. Moerdijk and Palmgren observe that every elementary topos with nno has W-types. This observation more than answers Schroeder's original question affirmatively. See Moerdijk and Palmgren, "Well-founded trees in categories", APAL 104, 2000, for the observation. I'm not sure whether they include the details (I don't have the paper to hand), but it's not a hard exercise. Alex Simpson Alex Simpson, LFCS, Division of Informatics, Univ. of Edinburgh Email: Alex.Simpson@ed.ac.uk Tel: +44 (0)131 650 5113 Web: http://www.dcs.ed.ac.uk/home/als Fax: +44 (0)131 667 7209