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

.

## Instances For

## Equations

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

## Equations

- PFunctor.instCoeFunForallType = { coe := PFunctor.Obj }

Applying `P`

to a morphism of `Type`

## Instances For

## Equations

- PFunctor.Obj.inhabited P = { default := ⟨default, default⟩ }

## Equations

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

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

root element of a W tree

## Instances For

children of the root of a W tree

## Instances For

destructor for W-types

## Instances For

constructor for W-types

## Equations

- PFunctor.W.mk x = match x with | ⟨a, f⟩ => WType.mk a f

## Instances For

## Equations

- PFunctor.Idx.inhabited P = { default := ⟨default, default⟩ }

`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

## Equations

- P₂.comp P₁ = { A := (a₂ : P₂.A) × (P₂.B a₂ → P₁.A), B := fun (a₂a₁ : (a₂ : P₂.A) × (P₂.B a₂ → P₁.A)) => (u : P₂.B a₂a₁.fst) × P₁.B (a₂a₁.snd u) }

## Instances For

constructor for composition

## Equations

- PFunctor.comp.mk P₂ P₁ x = ⟨⟨x.fst, Sigma.fst ∘ x.snd⟩, fun (a₂a₁ : (P₂.comp P₁).B ⟨x.fst, Sigma.fst ∘ x.snd⟩) => (x.snd a₂a₁.fst).snd a₂a₁.snd⟩

## Instances For

destructor for composition

## Equations

- PFunctor.comp.get P₂ P₁ x = ⟨x.fst.fst, fun (a₂ : P₂.B x.fst.fst) => ⟨x.fst.snd a₂, fun (a₁ : P₁.B (x.fst.snd a₂)) => x.snd ⟨a₂, a₁⟩⟩⟩