# How to define the natural numbers as a W-type?

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?

$$\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$.