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 : c.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 α.
@[instance]
Equations
- pfunctor.inhabited = {default := {A := inhabited.default (Type u_1) sort.inhabited, B := inhabited.default (inhabited.default (Type u_1) → Type u_1) (pi.inhabited (inhabited.default (Type u_1)))}}
@[instance]
Equations
- pfunctor.obj.inhabited P = {default := ⟨inhabited.default P.A _inst_1, λ (_x : P.B (inhabited.default P.A)), inhabited.default α⟩}
@[instance]
Equations
- _ = _
root element of a W tree
Equations
- pfunctor.W.head (W.mk a f) = a
children of the root of a W tree
Equations
- pfunctor.W.children (W.mk a f) = f
destructor for W-types
Equations
- pfunctor.W.dest (W.mk a f) = ⟨a, f⟩
constructor for W-types
Equations
- pfunctor.W.mk ⟨a, f⟩ = W.mk a f
@[simp]
@[instance]
def
pfunctor.Idx.inhabited
(P : pfunctor)
[inhabited P.A]
[inhabited (P.B (inhabited.default P.A))] :
Equations
- pfunctor.Idx.inhabited P = {default := ⟨inhabited.default P.A _inst_1, inhabited.default (P.B (inhabited.default P.A)) _inst_2⟩}
x.iget i takes the component of x designated by i if any is or returns
a default value
theorem
pfunctor.liftp_iff'
{P : pfunctor}
{α : Type u}
(p : α → Prop)
(a : P.A)
(f : P.B a → α) :
functor.liftp p ⟨a, f⟩ ↔ ∀ (i : P.B a), p (f i)
theorem
pfunctor.supp_eq
{P : pfunctor}
{α : Type u}
(a : P.A)
(f : P.B a → α) :
functor.supp ⟨a, f⟩ = f '' set.univ