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 : Type ?
- B : self.A → Type ?
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 pfunctor
- pfunctor.has_sizeof_inst
- pfunctor.inhabited
Equations
Applying P
to an object of Type
Instances for pfunctor.obj
Equations
- pfunctor.obj.inhabited P = {default := ⟨inhabited.default _inst_1, inhabited.default (pi.inhabited (P.B inhabited.default))⟩}
Equations
- pfunctor.obj.functor P = {map := P.map, map_const := λ (α β : Type u_2), P.map ∘ function.const β}
root element of a W tree
Equations
- pfunctor.W.head (W_type.mk a f) = a
children of the root of a W tree
Equations
- pfunctor.W.children (W_type.mk a f) = f
destructor for W-types
Equations
- pfunctor.W.dest (W_type.mk a f) = ⟨a, f⟩
constructor for W-types
Equations
- pfunctor.W.mk ⟨a, f⟩ = W_type.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
Instances for pfunctor.Idx
Equations
- pfunctor.Idx.inhabited P = {default := ⟨inhabited.default _inst_1, inhabited.default _inst_2⟩}
x.iget i
takes the component of x
designated by i
if any is or returns
a default value