snippetMinor
How to define the natural numbers as a W-type?
Viewed 0 times
thenumberstypenaturaldefinehow
Problem
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?
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?
Solution
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$.
$$\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$.
Context
StackExchange Computer Science Q#97179, answer score: 4
Revisions (0)
No revisions yet.