nLab W-type



Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logiccategory theorytype theory
trueterminal object/(-2)-truncated objecth-level 0-type/unit type
falseinitial objectempty type
proposition(-1)-truncated objecth-proposition, mere proposition
proofgeneralized elementprogram
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
cut elimination for implicationcounit for hom-tensor adjunctionbeta reduction
introduction rule for implicationunit for hom-tensor adjunctioneta conversion
logical conjunctionproductproduct type
disjunctioncoproduct ((-1)-truncation of)sum type (bracket type of)
implicationinternal homfunction type
negationinternal hom into initial objectfunction type into empty type
universal quantificationdependent productdependent product type
existential quantificationdependent sum ((-1)-truncation of)dependent sum type (bracket type of)
equivalencepath space objectidentity type/path type
equivalence classquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
completely presented setdiscrete object/0-truncated objecth-level 2-type/set/h-set
setinternal 0-groupoidBishop set/setoid
universeobject classifiertype of types
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels





A W-type is a set or type which is defined inductively in a well-founded way based on a type of “constructors” and a type of “arities”, with one constructor having a certain canonical form. As such it is a particular kind of 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. More complex inductive types, with multiple constructors that are assumed only to be strictly positive, can be reduced to W-types, at least in the presence of other structure such as sum types and function extensionality; see for instance AAG. This can even be extended to inductive families.

The terms/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} bB\{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 BB, and that if a node is labeled by bb then it has exactly |A b|{|A_b|} outgoing edges, each labeled by an element of A bA_b. From a more computational point of view, the W-type can be viewed as a data type, where BB indexes the set of constructors and A bA_b is the arity of the constructor bb.

If we remove the requirement that the trees are well-founded, we obtain instead a kind of coinductive type called an M-type (presumably since “M” is like a “W” upside down).


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

W-types in categories

Plain version

This version of W-types is the most natural for mathematicians used to thinking in terms of set theory or category theory, the categorical semantics of W-types, due to (Moerdijk-Palmgren 00).

Here we describe a W-type as the initial algebra for an endofunctor. The family {A b} bB\{A_b\}_{b\in B} can be thought of as a morphism f:ABf\colon A\to B in some category 𝒞\mathcal{C} (the fiber over bBb\in B being A bA_b), and the endofunctor in question is the composite

𝒞A *𝒞 /AΠ f𝒞 /BΣ B𝒞, \mathcal{C} \overset{A^*}{\longrightarrow} \mathcal{C}_{/A} \overset{\Pi_f}{\longrightarrow} \mathcal{C}_{/B} \overset{\Sigma_B}{\longrightarrow} \mathcal{C} \,,

where A *A^* is context extension, hence is the pullback functor (a.k.a. A×A\times -), Π f\Pi_f is a dependent product, and Σ B\Sigma_B is a dependent sum (a.k.a. the forgetful functor from 𝒞 /B\mathcal{C}_{/B} to 𝒞\mathcal{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 𝒞\mathcal{C} is not just locally cartesian closed but is a Π-pretopos, since often we want to use at least coproducts in constructing AA and BB. For example, a natural numbers object is a W-type specified by one of the coproduct inclusions 11+11\to 1+1, and the list object LXL X is a W-type specified by XX+1X\to X+1. More generally, endofunctors that look like polynomials in the traditional sense:

F(Y)=A n×Y ×n++A 1×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 SetSet is not a topos and W-types in it must be postulated explicitly).

Dependent W-types

The above has a natural generalization to dependent or indexed W-types (Gambino-Hyland 04) with a type CC of indices:

given a diagram of the form

A f B h g C C \array{ A &\stackrel{f}{\longrightarrow}& B \\ \downarrow^{\mathrlap{h}} && \downarrow^{\mathrlap{g}} \\ C && C }

there is the dependent polynomial functor

𝒞 /Ch *𝒞 /AΠ f𝒞 /BΣ g𝒞 /C, \mathcal{C}_{/C} \overset{h^\ast}{\longrightarrow} \mathcal{C}_{/A} \overset{\Pi_f}{\longrightarrow} \mathcal{C}_{/B} \overset{\Sigma_g}{\longrightarrow} \mathcal{C}_{/C} \,,

This reduces to the above for C=*C = \ast the terminal object.

Notice that we do not necessarily have gf=hg f = h, so this is not just simply a polynomial endofunctor of 𝒞/ C\mathcal{C}/_{C} considered as a lccc in its own right. If we do have gf=hg f = h, then CC is called a type of parameters instead of indices.

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=gf=g if and only if f(x)=g(x)f(x)=g(x) for all xx), 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 WW-types in extensional type theory are the following:

(1) WW-formation rule

A:Typex:AB(x):Type(Wx:A)B(x):Type\frac{A:Type\; x:A\vdash B(x):Type}{(W x:A)B(x):Type}

Andreas Abel: A and B are used exactly the other way round in the introductory text to this page. (Before, A was the arity, now B is the arity.) Harmonize!?

In the following we will sometimes abbreviate (Wx:A)B(x)(W x:A)B(x) by WW.

(2) WW-introduction rule

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

(3) WW-elimination rule

w:WC(w):Type x:A,u:B(x)W,v:(Πy:B(x))C(u(y)) c(x,u,v):C(sup(x,u))w:Wwrec(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,u,v):C(sup(x,u))}}{w:W\vdash wrec(w,c):C(w)}

(4) WW-computation rule

w:WC(w):Type x:A,u:B(x)W,v:(Πy:B(x))C(u(y)) c(x,u,v):C(sup(x,u))x:A,u:B(x)Wwrec(sup(x,u),c)= c(x,u,λy.wrec(u(y),c)):C(sup(x,u))\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,u,v):C(sup(x,u))}}{\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 ff (from the lines above the rules) must be assumed to be a display map, i.e. to exhibit AA as a dependent type over BB, in order that the dependent product Π f\Pi_f be defined.

In the case of dependent polynomial functors, it seems that qq must also be a display map, in order to define Σ q\Sigma_q. However, using adjointness, one can still define the W-type even if qq is not a display map. This more general version is what in type theory is called an indexed W-type; if qq is a display map then one sometimes refers to non-uniform parameters instead of indices. (By contrast, uniform parameters are the kind discussed above where gf=hg f = h, so that the entire construction takes place in a single slice category This is an instance of the red herring principle, since non-uniform parameters are not really parameters at all, but a special kind of indices.) For example, identity types are indexed W-types but not parametrized ones (even non-uniformly); see this blog post.)

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.


In homotopy type theory, if AA as h-level n1n\geq -1, then WABW A B has h-level nn (as it should be for (infinity,1)-colimits). A formal proof of this is discussed in (Danielsson).

type, type theory

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

homotopy type, homotopy type theory


The original definition in type theory is due to

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

The categorical semantics of W-types by initial algebras of polynomial endofunctors is due to

Dependent W-type were introduced in

  • Nicola Gambino, Martin Hyland, Wellfounded trees and dependent polynomial functors. In Types for proofs and programs, volume 3085 of Lecture Notes in Comput. Sci., pages 210–225. Springer-Verlag, Berlin, 2004 (web)

Related work is:

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

Work towards dependent W-types in HoTT is here; see also inductive families.

  • Christian Sattler, On relating indexed W-types with ordinary ones, 2015 PDF

A formal proof about the h-level of W-types is discussed in

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

and also in

which also computes the identity types of W-types (and more generally indexed W-types).

Discussion of W-types in homotopy type theory, or rather in model categories presenting homotopy theories, is in

W-types in Coq wiki

Last revised on August 15, 2021 at 13:07:43. See the history of this page for a list of all contributions to it.