# 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.obj α`

, which is defined as the sigma type `Σ x, P.B x → α`

.

An element of `P.obj α`

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 `α`

.

## Instances For

Applying `P`

to an object of `Type`

## Instances For

Applying `P`

to a morphism of `Type`

## Instances For

re-export existing definition of W-types and adapt it to a packaged definition of polynomial functor

## Instances For

children of the root of a W tree

## Instances For

destructor for W-types

## Instances For

constructor for W-types

## Instances For

`Idx`

identifies a location inside the application of a pfunctor.
For `F : PFunctor`

, `x : F.obj α`

and `i : F.Idx`

, `i`

can designate
one part of `x`

or is invalid, if `i.1 ≠ x.1`

## Instances For

`x.iget i`

takes the component of `x`

designated by `i`

if any is or returns
a default value

## Instances For

functor composition for polynomial functors

## Instances For

constructor for composition

## Instances For

destructor for composition