# Examples of W-types #

We take the view of W types as inductive types.
Given `α : Type`

and `β : α → Type→ Type`

, the W type determined by this data, `WType β`

, is the
inductively with constructors from `α`

and arities of each constructor `a : α`

given by `β a`

.

This file contains `Nat`

and `List`

as examples of W types.

## Main results #

`WType.equivNat`

: the construction of the naturals as a W-type is equivalent to`Nat`

`WType.equivList`

: the construction of lists on a type`γ`

as a W-type is equivalent to`List γ`

## Equations

- WType.instInhabitedNatα = { default := WType.Natα.zero }

The arity of the constructors for the naturals, `zero`

takes no arguments, `succ`

takes one

## Equations

- WType.Natβ x = match x with | WType.Natα.zero => Empty | WType.Natα.succ => Unit

## Equations

- WType.instInhabitedNatβSucc = { default := () }

The isomorphism from the naturals to its corresponding `WType`

## Equations

- WType.ofNat Nat.zero = WType.mk WType.Natα.zero Empty.elim
- WType.ofNat (Nat.succ n) = WType.mk WType.Natα.succ fun x => WType.ofNat n

The isomorphism from the `WType`

of the naturals to the naturals

## Equations

- WType.toNat (WType.mk WType.Natα.zero f) = 0
- WType.toNat (WType.mk WType.Natα.succ f) = Nat.succ (WType.toNat (f ()))

The naturals are equivalent to their associated `WType`

## Equations

- WType.equivNat = { toFun := WType.toNat, invFun := WType.ofNat, left_inv := WType.leftInverse_nat, right_inv := WType.rightInverse_nat }

`WType.Natα`

is equivalent to `PUnit ⊕ PUnit⊕ PUnit`

.
This is useful when considering the associated polynomial endofunctor.

## Equations

- One or more equations did not get rendered due to their size.

- nil: {γ : Type u} → WType.Listα γ
- cons: {γ : Type u} → γ → WType.Listα γ

The constructors for lists.
There is "one constructor `cons x`

for each `x : γ`

",
since we view `List γ`

as

```
| nil : List γ
| cons x₀ : List γ → List γ
| cons x₁ : List γ → List γ
| ⋮ γ many times
→ List γ
| cons x₁ : List γ → List γ
| ⋮ γ many times
→ List γ
| ⋮ γ many times
⋮ γ many times
```

## Instances For

## Equations

- WType.instInhabitedListα γ = { default := WType.Listα.nil }

The arities of each constructor for lists, `nil`

takes no arguments, `cons hd`

takes one

## Equations

- WType.Listβ γ x = match x with | WType.Listα.nil => PEmpty | WType.Listα.cons a => PUnit

## Equations

- WType.instInhabitedListβCons γ hd = { default := PUnit.unit }

The isomorphism from lists to the `WType`

construction of lists

## Equations

- WType.ofList γ [] = WType.mk WType.Listα.nil PEmpty.elim
- WType.ofList γ (hd :: tl) = WType.mk (WType.Listα.cons hd) fun x => WType.ofList γ tl

The isomorphism from the `WType`

construction of lists to lists

## Equations

- WType.toList γ (WType.mk WType.Listα.nil f) = []
- WType.toList γ (WType.mk (WType.Listα.cons hd) f) = hd :: WType.toList γ (f PUnit.unit)

Lists are equivalent to their associated `WType`

## Equations

- One or more equations did not get rendered due to their size.

`WType.Listα`

is equivalent to `γ`

with an extra point.
This is useful when considering the associated polynomial endofunctor

## Equations

- One or more equations did not get rendered due to their size.