# W types #

Given `α : Type`

and `β : α → Type→ Type`

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

, is the
inductively defined type of trees where the nodes are labeled by elements of `α`

and the children of
a node labeled `a`

are indexed by elements of `β a`

.

This file is currently a stub, awaiting a full development of the theory. Currently, the main result
is that if `α`

is an encodable fintype and `β a`

is encodable for every `a : α`

, then `WType β`

is
encodable. This can be used to show the encodability of other inductive types, such as those that
are commonly used to formalize syntax, e.g. terms and expressions in a given language. The strategy
is illustrated in the example found in the file `prop_encodable`

in the `archive/examples`

folder of
mathlib.

## Implementation details #

While the name `WType`

is somewhat verbose, it is preferable to putting a single character
identifier `W`

in the root namespace.

Given `β : α → Type _→ Type _`

, `WType β`

is the type of finitely branching trees where nodes are labeled by
elements of `α`

and the children of a node labeled `a`

are indexed by elements of `β a`

.

## Instances For

## Equations

- instInhabitedWTypeUnitEmpty = { default := WType.mk () Empty.elim }

The canonical map to the corresponding sigma type, returning the label of a node as an
element `a`

of `α`

, and the children of the node as a function `β a → WType β→ WType β`

.

## Equations

- WType.toSigma x = match x with | WType.mk a f => { fst := a, snd := f }

The canonical map from the sigma type into a `WType`

. Given a node `a : α`

, and
its children as a function `β a → WType β→ WType β`

, return the corresponding tree.

## Equations

- WType.ofSigma x = match x with | { fst := a, snd := f } => WType.mk a f

The canonical bijection with the sigma type, showing that `WType`

is a fixed point of
the polynomial functor `X ↦ Σ a : α, β a → X↦ Σ a : α, β a → X→ X`

.

## Equations

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

The canonical map from `WType β`

into any type `γ`

given a map `(Σ a : α, β a → γ) → γ→ γ) → γ→ γ`

.

## Equations

- WType.elim γ fγ (WType.mk a f) = fγ { fst := a, snd := fun b => WType.elim γ fγ (f b) }

The depth of a finitely branching tree.

## Equations

- WType.depth (WType.mk a f) = (Finset.sup Finset.univ fun n => WType.depth (f n)) + 1

`WType`

is encodable when `α`

is an encodable fintype and for every `a : α`

, `β a`

is
encodable.

## Equations

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