# 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

## Equations

- PFunctor.instInhabitedPFunctor = { default := { A := default, B := default } }

Applying `P`

to an object of `Type`

## Equations

- PFunctor.Obj P α = ((x : P.A) × (PFunctor.B P x → α))

Applying `P`

to a morphism of `Type`

## Equations

- PFunctor.map P f x = match x with | { fst := a, snd := g } => { fst := a, snd := f ∘ g }

## Equations

- PFunctor.Obj.inhabited P = { default := { fst := default, snd := default } }

## Equations

- PFunctor.instFunctorObj P = { map := @PFunctor.map P, mapConst := fun {α β} => PFunctor.map P ∘ Function.const β }

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

## Equations

- PFunctor.W P = WType P.B

root element of a W tree

## Equations

- PFunctor.W.head x = match x with | WType.mk a _f => a

children of the root of a W tree

## Equations

- PFunctor.W.children x = match (motive := (x : PFunctor.W P) → PFunctor.B P (PFunctor.W.head x) → PFunctor.W P) x with | WType.mk _a f => f

destructor for W-types

## Equations

- PFunctor.W.dest x = match x with | WType.mk a f => { fst := a, snd := f }

constructor for W-types

## Equations

- PFunctor.W.mk x = match x with | { fst := a, snd := f } => WType.mk a f

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

## Equations

- PFunctor.IdxCat P = ((x : P.A) × PFunctor.B P x)

## Equations

- PFunctor.IdxCat.inhabited P = { default := { fst := default, snd := default } }

`x.iget i`

takes the component of `x`

designated by `i`

if any is or returns
a default value

## Equations

- PFunctor.Obj.iget x i = if h : i.fst = x.fst then Sigma.snd P.A (fun x => PFunctor.B P x → α) x (cast (_ : PFunctor.B P i.fst = PFunctor.B P x.fst) i.snd) else default

constructor for composition

## Equations

- One or more equations did not get rendered due to their size.

destructor for composition

## Equations

- One or more equations did not get rendered due to their size.