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