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.