nLab W-type

W-types

Context

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

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
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

semantics

Induction

W-types

Idea

In type theory, by a 𝒲\mathcal{W}-type [Martin-LΓΆf (1982), pp. 171, (1984), pp. 43] one means a type which is defined inductively in a 𝒲 \mathcal{W} ell-founded way based on a type CC of β€œconstructors” and a type of AA of β€œarities”. As such, 𝒲\mathcal{W}-types are special kinds of inductive types (see below).

The same terminology β€œπ’²\mathcal{W}-type” is used [Moerdijk & Palmgren (2000)] for objects in (suitable pre-)toposes which provide categorical semantics for the type-theoretic notion (see further below).

Concretely, the terms/elements of a 𝒲\mathcal{W}-type may be thought of as β€œrooted well-founded trees” with a certain branching type; different 𝒲\mathcal{W}-types are distinguished by their branching signatures: In categorical semantics in Sets, a branching signature is represented by a family of sets {A c} c∈C\{A_c\}_{c \in C} such that

  • each node of the tree is labeled with an element c:Cc \colon C – referring to a constructor;

  • if a node is labeled by cc then it has exactly |A c|{|A_c|} outgoing edges, each labeled by some a:A ca \colon A_c – the arity of the constructor cc.

If one discards the requirement that the trees be well-founded, then the notion of 𝒲\mathcal{W}-type becomes that of a coinductive type called an M-type (presumably since β€œM” is like a β€œW” upside down).

In practice, 𝒲\mathcal{W}-types are used to:

  1. provide a constructive counterpart of the classical notion of a well-ordering

  2. uniformly define a variety of well-behaved inductive types.

More complex inductive types, with multiple constructors that are assumed only to be strictly positive, can be reduced to 𝒲\mathcal{W}-types, at least in the presence of other structure such as sum types and function extensionality; see for instance Abbott, Altenkirch & Ghani (2004). This can even be extended to inductive families.

In most set theoretic mathematical foundations, 𝒲\mathcal{W}-types can be proven to exist, but in predicative mathematics and in type theory, where this is not the case, they are often introduced axiomatically (as usual for inductive types more generally).

Definition

There are two slightly different formulations of W-types:

  1. 𝒲\mathcal{W}-types in type theory

  2. 𝒲\mathcal{W}-types in categories

𝒲\mathcal{W}-types in type theory

Definition

(inference rules for 𝒲\mathcal{W}-types)

(1) type formation rule:

C:Type;c:C⊒A(c):Type| || |𝒲c:CA(c):Type \frac { C \,\colon\, Type \;; \;\;\; c \,\colon\, C \;\;\vdash\;\; A(c) \,\colon\,Type \mathclap{\phantom{\vert_{\vert}}} } { \mathclap{\phantom{\vert^{\vert}}} \underset{c \colon C}{\mathcal{W}}\, A(c) \,\colon\, Type }

(2) term introduction rule:

⊒root:C;subtr:A(root)→𝒲c:CA(c)| |tree(root,subtr):𝒲c:CA(c) \frac{ \vdash\; root \,\colon\, C \;; \;\; subtr \,\colon\, A(root) \to \underset{c \colon C}{\mathcal{W}}\, A(c) }{ \mathclap{\phantom{\vert^{\vert}}} tree\big(root ,\, subtr\big) \,\colon\, \underset{c \colon C}{\mathcal{W}}\, A(c) }

(3) term elimination rule:

t:𝒲c:CA(c)⊒D(t):Type; root:C,subt:A(root)→𝒲c:CA(c),subt D:∏a:A(root)D(subt(a)) ⊒tree D(root,subt,subt D):D(tree(root,subt))| || |t:𝒲c:CA(c)⊒wrec (D,tree D)(t):D(t) \frac{ \begin{array}{l} t \,\colon\, \underset{c \colon C}{\mathcal{W}}\, A(c) \;\vdash\; D(t) \,\colon\, Type \;; \\ root \,\colon\, C \,, \; subt \,\colon\, A(root) \to \underset{c \colon C}{\mathcal{W}}\, A(c) \,, \; subt_D \,\colon\, \underset{a \colon A(root)}{\prod} D\big(subt(a)\big) \\ \;\;\;\;\;\;\;\;\;\;\;\;\;\;\; \;\;\vdash\;\; tree_D\big(root,\,subt ,\, subt_D\big) \,\colon\, D\big(tree(root,\, subt)\big) \mathclap{\phantom{\vert_{\vert}}} \end{array} }{ \mathclap{\phantom{\vert^{\vert}}} t \,\colon\, \underset{c \colon C}{\mathcal{W}}\, A(c) \;\vdash\; wrec_{(D,tree_D)}(t) \,\colon\, D(t) }

(4) computation rule:

t:𝒲c:CA(c)⊒D(t):Type; root:C,subt:A(root)→𝒲c:CA(c),subt D:Ξ a:A(c)D(subt(a)) ⊒tree D(root,subt,subt D):D(tree(root,subt))| || |root:C,subtr:A(root)→𝒲c:CA(c) ⊒wrec (D,tree D)(tree(root,subtr))=tree D(root,subt,Ξ»a.wrec (D,tree D)(subtr(a))) \frac{ \begin{array}{l} t \,\colon\, \underset{c \colon C}{\mathcal{W}}\, A(c) \;\vdash\; D(t) \,\colon\, Type \;; \\ root \,\colon\, C \,,\; subt \,\colon\, A(root) \to \underset{c \colon C}{\mathcal{W}}\, A(c) \,, \; subt_D \,\colon\, \underset{a\colon A(c)}{\Pi} D\big(subt(a)\big) \\ \;\;\;\;\;\;\;\;\;\;\;\;\;\;\; \;\;\vdash\;\; tree_D\big(root,\,subt,\,subt_D\big) \,\colon\, D\big(tree(root,\, subt)\big) \mathclap{\phantom{\vert_{\vert}}} \end{array} }{ \begin{array}{l} \mathclap{\phantom{\vert^{\vert}}} root \,\colon\, C \,, \;\; subtr \,\colon\, A(root) \to \underset{c \colon C}{\mathcal{W}}\, A(c) \\ \;\;\;\;\;\;\;\;\;\;\; \;\;\vdash\;\; wrec_{(D,tree_D)}\big( tree(root, \, subtr) \big) \;=\; tree_D \Big( root ,\, subt ,\, \lambda a . wrec_{(D,tree_D)}\big(subtr(a)\big) \Big) \end{array} }

(due to Martin-LΓΆf (1984), pp. 43; streamlined review e.g. in Awodey, Gambino & Sojakova (2012, Β§2))

Remark

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 1-category-theoretic definition below. The type theories that are the internal logic of familiar kinds of categories are all extensional in this sense.

The main distinction from the naive categorical theory below is that the map ff (1) 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.)

Remark

In intensional type theory, a 𝒲\mathcal{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 type (Exp. ).

𝒲\mathcal{W}-types in categories

Plain version

We discuss the categorical semantics of 𝒲\mathcal{W}-types, due to Moerdijk & Palmgren (2000).

Here one describes a 𝒲\mathcal{W}-type as an initial algebra for an endofunctor on an ambient category π’ž\mathcal{C}. The family {A c} c∈C\{A_c\}_{c\in C} can be thought of as a morphism

(1)A ↓f C \array{ A \\ \big\downarrow\mathrlap{^{f}} \\ C }

in some category π’ž\mathcal{C} (such that the fiber over c∈Cc\in C is A cA_c), and the endofunctor in question is the composite

π’žβŸΆA *π’ž /A⟢Π fπ’ž /C⟢Σ Cπ’ž, \mathcal{C} \overset{A^*}{\longrightarrow} \mathcal{C}_{/A} \overset{\Pi_f}{\longrightarrow} \mathcal{C}_{/C} \overset{\Sigma_C}{\longrightarrow} \mathcal{C} \,,

where

Equivalently, it is the composite

π’žβŸΆC *π’ž /CβŸΆβ—― fπ’ž /C⟢Σ Cπ’ž, \mathcal{C} \overset{C^*}{\longrightarrow} \mathcal{C}_{/C} \overset{\bigcirc_f}{\longrightarrow} \mathcal{C}_{/C} \overset{\Sigma_C}{\longrightarrow} \mathcal{C} \,,

where β—― f\bigcirc_f is the reader monad Ξ  f∘f *\Pi_f \circ f^*. In other words, the dependent product is not actually dependent.

Such a composite is called a polynomial endofunctor. Explicitly, it is the functor Xβ†¦βˆ‘ c:CX A cX \mapsto \sum_{c : C} X^{A_c}.

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.)

The above 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 CC. For example, a natural numbers object (Exp. ) is a 𝒲\mathcal{W}-type specified by one of the coproduct inclusions 1β†’1+11\to 1+1, and the list object LXL X is a 𝒲\mathcal{W}-type specified by Xβ†’X+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 for any lextensive category, and hence 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 𝒲\mathcal{W}-types

The above has a natural generalization to dependent or indexed W-types (Gambino & Hyland (2004)) 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

π’ž /C⟢h *π’ž /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 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.

Examples

Example

(natural numbers type as a 𝒲 \mathcal{W} -type)
The natural numbers type (β„•,0,succ)(\mathbb{N},\, 0,\, succ) is equivalently the 𝒲 \mathcal{W} -type (Def. ) with

  • C≔{0,succ}≃*βŠ”*C \,\coloneqq\, \{0, succ\} \,\simeq\, \ast \sqcup \ast;

  • A 0β‰”βˆ…A_0 \,\coloneqq\, \varnothing (empty type);

    A succ≔*A_{succ} \,\coloneqq\, \ast (unit type)

[Martin-LΓΆf (1984), pp. 45, Dybjer (1997, p. 330, 333)]

Properties

Proposition

(Danielsson (2012))
In homotopy type theory, if CC has h-level nβ‰₯βˆ’1n\geq -1, then any 𝒲\mathcal{W}-type of the form 𝒲CB\underset{C}{\mathcal{W}} B has h-level nn (as it should be for ∞ \infty -colimits).

type, type theory

dependent type, dependent type theory, Martin-LΓΆf dependent type theory

homotopy type, homotopy type theory

References

General

The original definition in type theory is due to

In homotopy type theory:

On the h-level of W-types:

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

W-types in Coq: wiki

Categorical semantics of 𝒲\mathcal{W}-types

The observation that the categorical semantics of well-founded inductive types ( 𝒲 \mathcal{W} -types) is given by initial algebras over polynomial endofunctors on the type system:

Further discussion:

Generalization to inductive families (dependent 𝒲\mathcal{W}-types):

Generalization to homotopy-initial algebras as categorical semantics for 𝒲 \mathcal{W} -types in homotopy type theory:

Towards combining generalization to dependent and homotopical W-types:

Last revised on February 27, 2024 at 21:35:10. See the history of this page for a list of all contributions to it.