# W types #

Given `α : Type`

and `β : α → 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*`

, `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

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) }

## Instances For

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