W-types in toposes

W-types in toposes

[Thomas Streicher]

Alex S. pointed out quite correctly that toposes with NNO allow one to
construct W-types Wx:A.B(x) for all  b : B -> A (where B(x) is a shorthand
for b^{-1}(x)). The idea is as follows: elements of Wx:A.B(x) are thought of
as well-founded terms over the signature A where B(a) is the arity of
operation with name a. Thus, possibly infinite terms over this signature can
be coded up as partial maps  t : List(B) \parr A  satisfying the conditions

  (i)  the domain of t is prefix closed

 (ii)  if t(s) is defined and equal a then t(s^y) is defined iff and only
       if y \in B(a)

The term t is ``reachable'' iff  dom(t)  is an element of the least subset
T_B of P(List(B)) satisfying the closure conditions

   -  {<>} in T_B

   -  if a \in A and f : B(a) -> T_B then
      {<>} \cup { b^s | b \in B(a) & s \in f(b) }

Notice that ``reachable'' is more restrictive than well-founded in a
constructive setting. Claiming that "well-founded entails reachable" is
known as "bar induction".

Generally, W-types capture inductive types which are of the type "free term
algebra" albeit for very general signatures as given by a family of types.
It certainly contains all and more than what one thinks of in C.S. usually
when using the word inductive type.
However, necessarily "inductive type" is an "open" notion and heavily
syntax-dependent. There is the categorical generalization of inductive type
as initial fixpoint of a covariant functor F : EE->EE where EE is the ambient
topos or model of type theory. In a sense this a vacuous notion as you can get
every type A as initial fixpoint of F(X)=A. On the other hand, even in Set not
every covariant functor F : Set->Set needs to have a fixpoint (e.g. if F is
the covariant powerset functor). However, sometimes in categories different
from Set functor of the form F(X) = S^(S^X) do have fixpoints for particular
nontrivial S (for Sierpinski space).

The reason why I mentioned axiom of replacement is that in the business of
solving recursive domain equations the axiom of relacement is needed (see
Alex Simpson's paper from LICS02). But in any case for constructing free term
algebras we don't need it.

Nevertheless, there is still a nagging question about the relationship between
inductive predicates and inductive types. Can one characterise those
syntactically given covaraint functors F (constructed, say, from parameters
using sum, cartesian product and exponentiation) for which HAH proves the
existence of a fixpoint, in other words which inductive types are ensured by
higher order arithmetic?

Thomas S.