Polynomial functors #
This file defines polynomial functors and the W-type construction as a polynomial functor. (For the M-type construction, see pfunctor/M.lean.)
A polynomial functor P
is given by a type A
and a family B
of types over A
. P
maps
any type α
to a new type P α
, which is defined as the sigma type Σ x, P.B x → α
.
An element of P α
is a pair ⟨a, f⟩
, where a
is an element of a type A
and
f : B a → α
. Think of a
as the shape of the object and f
as an index to the relevant
elements of α
.
- A : Type u
The head type
The child family of types
Applying P
to an object of Type
Equations
- PFunctor.instCoeFunForallType = { coe := PFunctor.Obj }
Equations
- P.instFunctorObj = { map := @PFunctor.map P }
We prefer PFunctor.map
to Functor.map
because it is universe-polymorphic.
re-export existing definition of W-types and adapt it to a packaged definition of polynomial functor
root element of a W tree
Equations
- PFunctor.W.head (WType.mk a _f) = a
children of the root of a W tree
Equations
- PFunctor.W.children (WType.mk a _f) = _f
destructor for W-types
Equations
- PFunctor.W.dest (WType.mk a _f) = ⟨a, _f⟩
constructor for W-types
Equations
- PFunctor.W.mk ⟨a, f⟩ = WType.mk a f