Multivariate polynomial functors.
Multivariate polynomial functors are used for defining M-types and W-types.
They map a type vector α to the type Σ a : A, B a ⟹ α, with A : Type and
B : A → typevec n. They interact well with Lean's inductive definitions because
they guarantee that occurrences of α are positive.
multivariate polynomial functors
Applying P to an object of Type
Applying P to a morphism of Type
@[instance]
Equations
- mvpfunctor.inhabited = {default := {A := inhabited.default (Type u_1) sort.inhabited, B := λ (_x : inhabited.default (Type u_1)), inhabited.default (typevec n)}}
@[instance]
def
mvpfunctor.obj.inhabited
{n : ℕ}
(P : mvpfunctor n)
{α : typevec n}
[inhabited P.A]
[Π (i : fin2 n), inhabited (α i)] :
Equations
- mvpfunctor.obj.inhabited P = {default := ⟨inhabited.default P.A _inst_1, λ (_x : fin2 n) (_x_1 : P.B (inhabited.default P.A) _x), inhabited.default (α _x)⟩}
theorem
mvpfunctor.map_eq
{n : ℕ}
(P : mvpfunctor n)
{α β : typevec n}
(g : α.arrow β)
(a : P.A)
(f : (P.B a).arrow α) :
mvfunctor.map g ⟨a, f⟩ = ⟨a, typevec.comp g f⟩
theorem
mvpfunctor.id_map
{n : ℕ}
(P : mvpfunctor n)
{α : typevec n}
(x : P.obj α) :
mvfunctor.map typevec.id x = x
theorem
mvpfunctor.comp_map
{n : ℕ}
(P : mvpfunctor n)
{α β γ : typevec n}
(f : α.arrow β)
(g : β.arrow γ)
(x : P.obj α) :
mvfunctor.map (typevec.comp g f) x = mvfunctor.map g (mvfunctor.map f x)
@[instance]
Equations
- _ = _
Constant functor where the input object does not affect the output
def
mvpfunctor.const.mk
(n : ℕ)
{A : Type u}
(x : A)
{α : typevec n} :
(mvpfunctor.const n A).obj α
Constructor for the constant functor
Equations
- mvpfunctor.const.mk n x = ⟨x, λ (i : fin2 n) (a : (mvpfunctor.const n A).B x i), pempty.elim a⟩
Destructor for the constant functor
Equations
- mvpfunctor.const.get x = x.fst
@[simp]
theorem
mvpfunctor.const.get_map
{n : ℕ}
{A : Type u}
{α β : typevec n}
(f : α.arrow β)
(x : (mvpfunctor.const n A).obj α) :
@[simp]
theorem
mvpfunctor.const.get_mk
{n : ℕ}
{A : Type u}
{α : typevec n}
(x : A) :
mvpfunctor.const.get (mvpfunctor.const.mk n x) = x
@[simp]
theorem
mvpfunctor.const.mk_get
{n : ℕ}
{A : Type u}
{α : typevec n}
(x : (mvpfunctor.const n A).obj α) :
mvpfunctor.const.mk n (mvpfunctor.const.get x) = x
Functor composition on polynomial functors
Constructor for functor composition
def
mvpfunctor.comp.get
{n m : ℕ}
{P : mvpfunctor n}
{Q : fin2 n → mvpfunctor m}
{α : typevec m} :
Destructor for functor composition
theorem
mvpfunctor.comp.get_map
{n m : ℕ}
{P : mvpfunctor n}
{Q : fin2 n → mvpfunctor m}
{α β : typevec m}
(f : α.arrow β)
(x : (P.comp Q).obj α) :
mvpfunctor.comp.get (mvfunctor.map f x) = mvfunctor.map (λ (i : fin2 n) (x : (Q i).obj α), mvfunctor.map f x) (mvpfunctor.comp.get x)
@[simp]
theorem
mvpfunctor.comp.get_mk
{n m : ℕ}
{P : mvpfunctor n}
{Q : fin2 n → mvpfunctor m}
{α : typevec m}
(x : P.obj (λ (i : fin2 n), (Q i).obj α)) :
@[simp]
theorem
mvpfunctor.comp.mk_get
{n m : ℕ}
{P : mvpfunctor n}
{Q : fin2 n → mvpfunctor m}
{α : typevec m}
(x : (P.comp Q).obj α) :
theorem
mvpfunctor.liftp_iff'
{n : ℕ}
{P : mvpfunctor n}
{α : typevec n}
(p : Π ⦃i : fin2 n⦄, α i → Prop)
(a : P.A)
(f : (P.B a).arrow α) :
mvfunctor.liftp p ⟨a, f⟩ ↔ ∀ (i : fin2 n) (x : P.B a i), p (f i x)
theorem
mvpfunctor.supp_eq
{n : ℕ}
{P : mvpfunctor n}
{α : typevec n}
(a : P.A)
(f : (P.B a).arrow α)
(i : fin2 n) :
mvfunctor.supp ⟨a, f⟩ i = f i '' set.univ
Split polynomial functor, get a n-ary functor
from a n+1-ary functor
def
mvpfunctor.append_contents
{n : ℕ}
(P : mvpfunctor (n + 1))
{α : typevec n}
{β : Type u_1}
{a : P.A} :
append arrows of a polynomial functor application
Equations
- P.append_contents f' f = typevec.split_fun f' f