Polynomial Functors #
This file defines polynomial functors and the W-type construction as a polynomial functor.
(For the M-type construction, see Mathlib/Data/PFunctor/Univariate/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 uA
The head type
The child family of types
Instances For
Applying P
to an object of Type
Instances For
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.
Instances For
x.iget i
takes the component of x
designated by i
if any is or returns a default value
Instances For
Composition for polynomial functors
Equations
Instances For
Constructor for composition
Equations
Instances For
Destructor for composition