\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{W-type}

\hypertarget{context}{}\subsubsection*{{Context}}\label{context}

\hypertarget{type_theory}{}\paragraph*{{Type theory}}\label{type_theory}

[[!include type theory - contents]]

\hypertarget{induction}{}\paragraph*{{Induction}}\label{induction}

[[!include induction - contents]]

\hypertarget{wtypes}{}\section*{{W-types}}\label{wtypes}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{examples}{Examples}\dotfill \pageref*{examples} \linebreak
\noindent\hyperlink{Definition}{Definition}\dotfill \pageref*{Definition} \linebreak
\noindent\hyperlink{wtypes_in_categories}{W-types in categories}\dotfill \pageref*{wtypes_in_categories} \linebreak
\noindent\hyperlink{plain_version}{Plain version}\dotfill \pageref*{plain_version} \linebreak
\noindent\hyperlink{DependentWTypesCategoricalSemantics}{Dependent W-types}\dotfill \pageref*{DependentWTypesCategoricalSemantics} \linebreak
\noindent\hyperlink{wtypes_in_type_theory}{W-types in type theory}\dotfill \pageref*{wtypes_in_type_theory} \linebreak
\noindent\hyperlink{Properties}{Properties}\dotfill \pageref*{Properties} \linebreak
\noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


\hypertarget{idea}{}\subsection*{{Idea}}\label{idea}

A \emph{W-type} is a [[set]] or [[type]] which is defined [[induction|inductively]] in a [[well-founded relation|well-founded]] way -- an [[inductive type]]. In most [[set theory|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 mathematics|constructive]] counterpart of the [[classical logic|classical]] notion of a [[well-ordering]] and to uniformly define a variety of [[inductive types]]. More complex inductive types, such as strictly positive inductive types, can be reduced to W-types; see \hyperlink{AAG}{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\}_{b\in B}$ which can be interpreted as requiring that each \emph{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 ${|A_b|}$ 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 \emph{constructors} and $A_b$ is the \emph{arity} of the constructor $b$.

If the trees are not required to be well-founded, we obtain instead a [[coinduction|coinductively]] defined type, called a ``co-W-type'' or an [[M-type]].

\hypertarget{examples}{}\subsection*{{Examples}}\label{examples}

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

\begin{itemize}%
\item $0$ of arity zero, and
\item $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.

\end{itemize}
(2) Similarly, if $X$ is any set, then the W-type $L X$ of [[lists]] of elements of $X$ has $|X|+1$ constructors:

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

\end{itemize}
(3) [[identity type]]s arise as a more general kind of W-type; see \href{http://homotopytypetheory.org/2011/04/18/whats-special-about-identity-types/}{this blog post}.

\hypertarget{Definition}{}\subsection*{{Definition}}\label{Definition}

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

\hypertarget{wtypes_in_categories}{}\subsubsection*{{W-types in categories}}\label{wtypes_in_categories}

\hypertarget{plain_version}{}\paragraph*{{Plain version}}\label{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 (\hyperlink{MoerdijkPalmgren00}{Moerdijk-Palmgren 00}).

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

\begin{displaymath}
\mathcal{C} \overset{A^*}{\longrightarrow} \mathcal{C}_{/A} \overset{\Pi_f}{\longrightarrow} \mathcal{C}_{/B} \overset{\Sigma_B}{\longrightarrow} \mathcal{C}
  \,,
\end{displaymath}
where $A^*$ is [[context extension]], hence 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 $\mathcal{C}_{/B}$ to $\mathcal{C}$).

Such a composite is called a \emph{[[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 category|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]] $L X$ is a W-type specified by $X\to X+1$. More generally, endofunctors that look like [[polynomial]]s in the traditional sense:

\begin{displaymath}
F(Y) = A_n \times Y^{\times n}  + \dots + A_1 \times Y  + A_0
\end{displaymath}
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 \textbf{[[Π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 [[predicative mathematics|predicativist]], in which case $Set$ is not a topos and W-types in it must be postulated explicitly).

\hypertarget{DependentWTypesCategoricalSemantics}{}\paragraph*{{Dependent W-types}}\label{DependentWTypesCategoricalSemantics}

The above has a natural generalization to [[dependent type|dependent]] W-types (\hyperlink{GambinoHyland04}{Gambino-Hyland 04}):

given a [[diagram]] of the form

\begin{displaymath}
\itexarray{
    A &\stackrel{f}{\longrightarrow}& B
    \\
    \downarrow^{\mathrlap{h}} && \downarrow^{\mathrlap{g}}
    \\
    C && C
  }
\end{displaymath}
there is the \emph{[[dependent polynomial functor]]}

\begin{displaymath}
\mathcal{C}_{/C} \overset{h^\ast}{\longrightarrow} 
  \mathcal{C}_{/A} 
    \overset{\Pi_f}{\longrightarrow} 
  \mathcal{C}_{/B} 
    \overset{\Sigma_g}{\longrightarrow} 
  \mathcal{C}_{/C}
  \,,
\end{displaymath}
This reduces to the above for $C = \ast$ the [[terminal object]]. Notice that we do not necessarily have $g f \simeq h$, so this is not just simply a polynomial endofunctor of $\mathcal{C}/_{C}$ considered as a lccc in its own right.

\hypertarget{wtypes_in_type_theory}{}\subsubsection*{{W-types in type theory}}\label{wtypes_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 \emph{[[extensional type theory|extensional]]}, i.e. [[identity type|identities]] have unique proofs and (dependent) [[function types]] are [[function extensionality|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

\begin{displaymath}
\frac{A:Type\; x:A\vdash B(x):Type}{(W x:A)B(x):Type}
\end{displaymath}
[[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 $(W x:A)B(x)$ by $W$.

(2) $W$-introduction rule

\begin{displaymath}
\frac{a:A\; t:B(a)\to W}{sup(a,t):W}
\end{displaymath}
(3) $W$-elimination rule

\begin{displaymath}
\frac{\itexarray{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)}
\end{displaymath}
(4) $W$-computation rule

\begin{displaymath}
\frac{\itexarray{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))}}{\itexarray{
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))}}
\end{displaymath}
(\hyperlink{AwodeyGambinoSojakova}{Awodey-Gambino-Sojakova} \S{}2, originally from \hyperlink{Martin-LofITT}{Martin-L\"o{}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 [[adjunction|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 type]]s arise as this more general kind of W-type; see \href{http://homotopytypetheory.org/2011/04/18/whats-special-about-identity-types/}{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.

\hypertarget{Properties}{}\subsection*{{Properties}}\label{Properties}

In [[homotopy type theory]], if $A$ as h-level $n\geq -1$, then $W A B$ has h-level $n$ (as it should be for [[(infinity,1)-colimits]]). A formal proof of this is discussed in (\hyperlink{Danielsson}{Danielsson}).

\hypertarget{related_concepts}{}\subsection*{{Related concepts}}\label{related_concepts}

\begin{itemize}%
\item [[M-type]]


\item [[predicative topos]]



\end{itemize}
[[!include notions of type]]

\hypertarget{references}{}\subsection*{{References}}\label{references}

The original definition in [[type theory]] is due to

\begin{itemize}%
\item [[Per Martin-Löf]], \emph{Intuitionistic Type Theory}, Notes by G. Sambin of a series of lectures given in Padua, 1980. Bibliopolis, 1984.

\end{itemize}
The [[categorical semantics]] of W-types by initial algebras of polynomial endofunctors is due to

\begin{itemize}%
\item [[Ieke Moerdijk]], [[Erik Palmgren]], \emph{Wellfounded trees in categories}, Annals of Pure and Applied Logic 104 (2000) 189 -- 218 (\href{http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.44.6700}{web})

\end{itemize}
\begin{itemize}%
\item [[Benno van den Berg]], [[Ieke Moerdijk]] (2008-09-25); \emph{$W$-types in sheaves}; \href{http://www.phil.cmu.edu/projects/ast/Papers/}{vdBM\_Wtypes.ps/pdf}

\end{itemize}
Dependent W-type were introduced in

\begin{itemize}%
\item [[Nicola Gambino]], [[Martin Hyland]], \emph{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 (\href{http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.98.4534}{web})

\end{itemize}
Related work is:

\begin{itemize}%
\item [[Michael Abbott]], [[Thorsten Altenkirch]], and [[Neil Ghani]], \emph{Representing Nested Inductive Types using W-types} (\href{http://www.cs.nott.ac.uk/~psztxa/publ/icalp04.pdf}{pdf})

\end{itemize}
Discussion in relation to [[identity types]] and [[homotopy type theory]] is in

\begin{itemize}%
\item [[Steve Awodey]], [[Nicola Gambino]], [[Kristina Sojakova]], \emph{Inductive types in homotopy type theory} (\href{http://arxiv.org/abs/1201.3898}{arXiv:1201.3898})


\item [[Steve Awodey]], [[Nicola Gambino]], [[Kristina Sojakova]], \emph{Homotopy-initial algebras in type theory} (\href{http://arxiv.org/abs/1504.05531}{arXiv:1504.05531})



\end{itemize}
Work towards dependent W-types in HoTT is here; see also [[inductive families]].

\begin{itemize}%
\item Christian Sattler, \emph{On relating indexed W-types with ordinary ones}, 2015 \href{http://cs.ioc.ee/types15/abstracts-book/contrib31.pdf}{PDF}

\end{itemize}
A formal proof about the [[h-level]] of W-types is discussed in

\begin{itemize}%
\item Nils Anders Danielsson, \emph{Positive h-levels are closed under W} (\href{https://homotopytypetheory.org/2012/09/21/positive-h-levels-are-closed-under-w/}{web})

\end{itemize}
Discussion of W-types in [[homotopy type theory]], or rather in [[model categories]] presenting [[homotopy theories]], is in

\begin{itemize}%
\item [[Benno van den Berg]], [[Ieke Moerdijk]], \emph{W-types in Homotopy Type Theory} (\href{http://arxiv.org/abs/1307.2765}{arXiv:1307.2765})

\end{itemize}
W-types in [[Coq]] \href{https://coq.inria.fr/cocorico/WTypeInsteadOfInductiveTypes}{wiki}

[[!redirects W-types]]



\end{document}