nLab
W-type

Idea

A W-type is a set or type which is defined inductively in a well-founded way – an inductive type. In most set theories, W-types can be proven to exist, but in predicative mathematics or type theory, where this is not the case, they are often assumed explicitly to exist. In particular W-types can be used to provide a constructive counterpart of the classical notion of a well-ordering and to uniformly define a variety of inductive types.

The elements of a W-type can be considered to be “rooted well-founded trees” with a certain branching type; different W-types are distinguished by their branching signatures. A branching signature is represented essentially by a family of sets $\{A_b{\}}_{b\in B}$ which can be interpreted as requiring that each node of the tree is labeled with an element of the set $B$, and that if a node is labeled by $b$ then it has exactly $\mid A_b\mid$ outgoing edges, each labeled by an element of $A_b$. From a more computational point of view, the W-type can be viewed as a data type, where $B$ indexes the set of constructors and $A_b$ is the arity of the constructor $b$.

If the trees are not required to be well-founded, we obtain instead a coinductively defined type, called a “co-W-type” or an M-type.

Examples

(1) The most basic W-type is the natural numbers. Here there are two constructors:

• $0$ of arity zero, and
• $S$ of arity one. Therefore, zero is a natural number, any natural number has a successor, and all natural numbers are generated in this way.

(2) Similarly, if $X$ is any set, then the W-type $LX$ of lists of elements of $X$ has $\mid X\mid +1$ constructors:

• $\mathrm{nil}$ of arity zero, and
• $\mathrm{cons}(x,-)$ of arity one, for each $x\in X$. Therefore, $\mathrm{nil}$ is a list, $\mathrm{cons}(x,\ell )$ is a list for any list $\ell$ and $x\in X$, and all lists are generated in this way.

(3) identity types arise as a more general kind of W-type; see this blog post.)

Definition

Actually, there are two slightly different formulations of W-types.

W-types in categories

This version of W-types is the most natural for mathematicians used to thinking in terms of set theory or category theory. Here we describe a W-type as the initial algebra for an endofunctor. The family $\{A_b{\}}_{b\in B}$ can be thought of as a morphism $f:A\to B$ in some category $C$ (the fiber over $b\in B$ being $A_b$), and the endofunctor in question is the composite

$$C\stackrel{A^{*}}{\to }C/A\stackrel{{\Pi }_f}{\to }C/B\stackrel{{\Sigma }_B}{\to }C.$$C \overset{A^*}{\to} C/A \overset{\Pi_f}{\to} C/B \overset{\Sigma_B}{\to} C.

Here $A^{*}$ is the pullback functor (a.k.a. $A\times -$), ${\Pi }_f$ is a dependent product, and ${\Sigma }_B$ is a dependent sum (a.k.a. the forgetful functor from $C/B$ to $C$).
Such a composite is called a polynomial endofunctor.

This definition makes sense in any locally cartesian closed category, although the W-type (the initial algebra) may or may not exist in any given such category. (A non-elementary construction of them is given by the transfinite construction of free algebras.)

This definition is most useful when the category $C$ is not just locally cartesian closed but is a Π-pretopos, since often we want to use at least coproducts in constructing $A$ and $B$. For example, a natural numbers object is a W-type specified by one of the coproduct inclusions $1\to 1+1$, and the list object $LX$ is a W-type specified by $X\to X+1$. More generally, endofunctors that look like polynomials in the traditional sense:

$$F(Y)=A_n\times Y^{\times n}+\dots +A_1\times Y+A_0$$F(Y) = A_n \times Y^{\times n} + \dots + A_1 \times Y + A_0

can be constructed as polynomial endofunctors in the above sense in any $\Pi$-pretopos. A $\Pi$-pretopos in which all W-types exist is called a ΠW-pretopos.

In a topos with a natural numbers object (NNO), W-types for any polynomial endofunctor can be constructed as certain sets of well-founded trees; thus every topos with a NNO is a ΠW-pretopos. This applies in particular in the topos Set (unless one is a predicativist, in which case $\mathrm{Set}$ is not a topos and W-types in it must be postulated explicitly).

W-types can also be generalized to initial algebras for dependent polynomial functors, which are given by composites

$$C/D\stackrel{p^{*}}{\to }C/A\stackrel{{\Pi }_f}{\to }C/B\stackrel{{\Sigma }_q}{\to }C/D$$C/D \overset{p^*}{\to} C/A \overset{\Pi_f}{\to} C/B \overset{\Sigma_q}{\to} C/D

for some morphisms

$$D\stackrel{p}{\leftarrow }A\stackrel{f}{\to }B\stackrel{q}{\to }D.$$D \overset{p}{\leftarrow} A \overset{f}{\to} B \overset{q}{\to} D.

Note that we do not necessarily have $qf=p$, so this is not just simply a polynomial endofunctor of $C/D$ considered as a lccc in its own right.

W-types in type theory

In type theory, W-types are introduced by giving explicit constructors and destructors, a.k.a. term introduction and term elimination rules. If the type theory is extensional, i.e. identities have unique proofs and (dependent) function types are extensional ($f=g$ if and only if $f(x)=g(x)$ for all $x$), then this is more or less equivalent to the categorical version given above. The type theories that are the internal logic of familiar kinds of categories are all extensional in this sense.

The rules for $W$-types in extensional type theory are the following:

(1) $W$-formation rule

$$\frac{A:\mathrm{Type}x:A⊢B(x):\mathrm{Type}}{(\mathrm{Wx}:A)B(x):\mathrm{Type}}$$\frac{A:Type\; x:A\vdash B(x):Type}{(Wx:A)B(x):Type}

In the following we will sometimes abbreviate $(\mathrm{Wx}:A)B(x)$ by $W$.

(2) $W$-introduction rule

$$\frac{a:At:B(a)\to W}{\sup (a,t):W}$$\frac{a:A\; t:B(a)\to W}{sup(a,t):W}

(3) $W$-elimination rule

$$\frac{\begin{array}{c}w:W⊢C(w):\mathrm{Type}\\ x:A,u:B(x)\to W,v:(\Pi y:B(x))C(u(y))⊢\\ c(x,y,v):C(\sup (x,y))\end{array}}{w:W⊢\mathrm{wrec}(w,c):C(w)}$$\frac{\array{w:W\vdash C(w):Type\\ x:A, u:B(x)\to W, v:(\Pi y:B(x))C(u(y))\vdash\\ c(x,y,v):C(sup(x,y))}}{w:W\vdash wrec(w,c):C(w)}

(4) $W$-computation rule

$$\frac{\begin{array}{c}w:W⊢C(w):\mathrm{Type}\\ x:A,u:B(x)\to W,v:(\Pi y:B(x))C(u(y))⊢\\ c(x,y,v):C(\sup (x,y))\end{array}}{\begin{array}{c}x:A,u:B(x)\to W⊢\mathrm{wrec}(\sup (x,u),c)=\\ c(x,u,\lambda y.\mathrm{wrec}(u(y),c)):C(\sup (x,u))\end{array}}$$\frac{\array{w:W\vdash C(w):Type\\ x:A, u:B(x)\to W, v:(\Pi y:B(x))C(u(y))\vdash\\ c(x,y,v):C(sup(x,y))}}{\array{ x:A, u:B(x)\to W\vdash wrec(sup(x,u),c)=\\ c(x,u,\lambda y.wrec(u(y),c)):C(sup(x,u))}}

(Awodey-Gambino-Sojakova §2, originally from Martin-Löf)

The main distinction from the naive categorical theory above is that the map $f$ (from the lines above the rules) must be assumed to be a display map, i.e. to exhibit $A$ as a dependent type over $B$, in order that the dependent product ${\Pi }_f$ be defined. In the case of dependent polynomial functors, $q$ must also be a display map in order to define ${\Sigma }_q$. (Actually, using adjointness, one can still define the W-type even if $q$ is not a display map, but its properties are not as good. This extra generality is important, however. For example, identity types arise as this more general kind of W-type; see this blog post.)

Mike Shulman: Is the term “W-type” still used in this generality? Or are they just called “inductive types”?

Note also that in intensional type theory, a W-type is only an initial algebra with respect to propositional equality, not definitional equality. In particular, the constructors are injective only propositionally, not definitionally. This applies already for the natural numbers.

Properties

Formation of W-types in homotopy type theory only increases h-level (as it should be for (infinity,1)-colimits). A formal proof of this is discussed in (Danielsson).

Related concepts

• M-type

• predicative topos

type, type theory

• propositions as types, inductive type, W-type

dependent type, dependent type theory, Martin-Löf dependent type theory

homotopy type, homotopy type theory

• identity type, higher inductive type

References

• Ieke Moerdijk, Erik Palmgren, Wellfounded trees in categories (web)

• Benno van den Berg, Ieke Moerdijk (2008-09-25); $W$-types in sheaves; vdBM_Wtypes.ps/pdf

• Martin-Löf, Intuitionistic Type Theory. Notes by G. Sambin of a series of lectures given in Padua, 1980. Bibliopolis, 1984.

A formal proof that formation for W-types only increases h-level is discussed in

• Nils Anders Danielsson, Positive h-levels are closed under W

Discussion in relation to identity types and homotopy type theory is in

• Steve Awodey, Nicola Gambino, Kristina Sojakova, Inductive types in homotopy type theory (arXiv:1201.3898)