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.