# 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

## 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 β`

.

## Equations

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

## Instances For

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

. Given a node `a : α`

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

, return the corresponding tree.

## Equations

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

## Instances For

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

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

.

## Equations

- WType.equivSigma β = { toFun := WType.toSigma, invFun := WType.ofSigma, left_inv := ⋯, right_inv := ⋯ }

## 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 : β a) => 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 : β a) => WType.depth (f n)) + 1