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

.

## 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 | ⟨a, 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γ ⟨a, fun (b : β a) => WType.elim γ fγ (f b)⟩

## Instances For

`WType`

is encodable when `α`

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

, `β a`

is
encodable.

## Equations

- WType.instEncodable = let f := fun (t : WType β) => ⟨t.depth, ⟨t, ⋯⟩⟩; let finv := fun (p : (n : ℕ) × WType.WType' β n) => ↑p.snd; let_fun this := ⋯; Encodable.ofLeftInverse f finv this