I'm having trouble understanding the rules for W-types in type theory as defined here: https://ncatlab.org/nlab/show/W-type#wtypes_in_type_theory

Can someone give an example of how these rules could be used to define a simple W-type such as the natural numbers? What would $A$ and $B$ be in the formation rule for instance?


The formation and introduction rules for W-types, as given on n-cat lab, are:

$$\frac{A:Type\quad x:A⊦B:Type}{(W x:A)B(x):Type}-\text{Formation}$$

$$\frac{a:A\quad t:B(a)\rightarrow W}{sup(a,t):W}-\text{Introduction}$$

You can define the natural numbers by setting $A=Bool$ and $B(a) = \text{if}\; a\; \text{then}\; ⟂\; \text{else}\; Unit$. Where $⟂$ is the empty type and $Unit$ is the unit type.

Zero is then $sup(a,t)$ where $a=true$ and $t: ⟂ \rightarrow Nat = λn. abort(n)$. eg. we use the zero constructor (by choosing $a=true$) and fill in the only possible value of a function from $⟂$ to $Nat$.

The successor of $p$ can be defined as $a=false$, $t:Unit \rightarrow Nat = λx.p$.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.