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.

structure MvPFunctor (n : ℕ) : Type (u + 1)

multivariate polynomial functors

• A : Type u

  The head type

• B : self.A → TypeVec.{u} n

  The child family of types

def MvPFunctor.Obj {n : ℕ} (P : MvPFunctor.{u} n) (α : TypeVec.{u} n) : Type u

Applying P to an object of Type

instance MvPFunctor.instCoeFunForallTypeVecType {n : ℕ} : CoeFun (MvPFunctor.{u} n) fun (x : MvPFunctor.{u} n) => TypeVec.{u} n → Type u

def MvPFunctor.map {n : ℕ} (P : MvPFunctor.{u} n) {α β : TypeVec.{u} n} (f : α.Arrow β) : ↑P α → ↑P β

Applying P to a morphism of Type

instance MvPFunctor.instInhabited {n : ℕ} : Inhabited (MvPFunctor.{u_1} n)

instance MvPFunctor.Obj.inhabited {n : ℕ} (P : MvPFunctor.{u} n) {α : TypeVec.{u} n} [Inhabited P.A] [(i : Fin2 n) → Inhabited (α i)] : Inhabited (↑P α)

instance MvPFunctor.instMvFunctorObj {n : ℕ} (P : MvPFunctor.{u} n) : MvFunctor ↑P

theorem MvPFunctor.map_eq {n : ℕ} (P : MvPFunctor.{u} n) {α β : TypeVec.{u} 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.{u} n) {α : TypeVec.{u} n} (x : ↑P α) : MvFunctor.map TypeVec.id x = x

theorem MvPFunctor.comp_map {n : ℕ} (P : MvPFunctor.{u} n) {α β γ : TypeVec.{u} n} (f : α.Arrow β) (g : β.Arrow γ) (x : ↑P α) : MvFunctor.map (TypeVec.comp g f) x = MvFunctor.map g (MvFunctor.map f x)

instance MvPFunctor.instLawfulMvFunctorObj {n : ℕ} (P : MvPFunctor.{u} n) : LawfulMvFunctor ↑P

def MvPFunctor.const (n : ℕ) (A : Type u) : MvPFunctor.{u} n

Constant functor where the input object does not affect the output

def MvPFunctor.const.mk (n : ℕ) {A : Type u} (x : A) {α : TypeVec.{u} n} : ↑(const n A) α

Constructor for the constant functor

def MvPFunctor.const.get {n : ℕ} {A : Type u} {α : TypeVec.{u} n} (x : ↑(const n A) α) : A

Destructor for the constant functor

@[simp]

theorem MvPFunctor.const.get_map {n : ℕ} {A : Type u} {α β : TypeVec.{u} n} (f : α.Arrow β) (x : ↑(const n A) α) : get (MvFunctor.map f x) = get x

@[simp]

theorem MvPFunctor.const.get_mk {n : ℕ} {A : Type u} {α : TypeVec.{u} n} (x : A) : get (mk n x) = x

@[simp]

theorem MvPFunctor.const.mk_get {n : ℕ} {A : Type u} {α : TypeVec.{u} n} (x : ↑(const n A) α) : mk n (get x) = x

def MvPFunctor.comp {n m : ℕ} (P : MvPFunctor.{u} n) (Q : Fin2 n → MvPFunctor.{u} m) : MvPFunctor.{u} m

Functor composition on polynomial functors

def MvPFunctor.comp.mk {n m : ℕ} {P : MvPFunctor.{u} n} {Q : Fin2 n → MvPFunctor.{u} m} {α : TypeVec.{u} m} (x : ↑P fun (i : Fin2 n) => ↑(Q i) α) : ↑(P.comp Q) α

Constructor for functor composition

def MvPFunctor.comp.get {n m : ℕ} {P : MvPFunctor.{u} n} {Q : Fin2 n → MvPFunctor.{u} m} {α : TypeVec.{u} m} (x : ↑(P.comp Q) α) : ↑P fun (i : Fin2 n) => ↑(Q i) α

Destructor for functor composition

theorem MvPFunctor.comp.get_map {n m : ℕ} {P : MvPFunctor.{u} n} {Q : Fin2 n → MvPFunctor.{u} m} {α β : TypeVec.{u} m} (f : α.Arrow β) (x : ↑(P.comp Q) α) : get (MvFunctor.map f x) = MvFunctor.map (fun (i : Fin2 n) (x : ↑(Q i) α) => MvFunctor.map f x) (get x)

@[simp]

theorem MvPFunctor.comp.get_mk {n m : ℕ} {P : MvPFunctor.{u} n} {Q : Fin2 n → MvPFunctor.{u} m} {α : TypeVec.{u} m} (x : ↑P fun (i : Fin2 n) => ↑(Q i) α) : get (mk x) = x

@[simp]

theorem MvPFunctor.comp.mk_get {n m : ℕ} {P : MvPFunctor.{u} n} {Q : Fin2 n → MvPFunctor.{u} m} {α : TypeVec.{u} m} (x : ↑(P.comp Q) α) : mk (get x) = x

theorem MvPFunctor.liftP_iff {n : ℕ} {P : MvPFunctor.{u} n} {α : TypeVec.{u} n} (p : ⦃i : Fin2 n⦄ → α i → Prop) (x : ↑P α) : MvFunctor.LiftP p x ↔ ∃ (a : P.A) (f : (P.B a).Arrow α), x = ⟨a, f⟩ ∧ ∀ (i : Fin2 n) (j : P.B a i), p (f i j)

theorem MvPFunctor.liftP_iff' {n : ℕ} {P : MvPFunctor.{u} n} {α : TypeVec.{u} 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.liftR_iff {n : ℕ} {P : MvPFunctor.{u} n} {α : TypeVec.{u} n} (r : ⦃i : Fin2 n⦄ → α i → α i → Prop) (x y : ↑P α) : MvFunctor.LiftR r x y ↔ ∃ (a : P.A) (f₀ : (P.B a).Arrow α) (f₁ : (P.B a).Arrow α), x = ⟨a, f₀⟩ ∧ y = ⟨a, f₁⟩ ∧ ∀ (i : Fin2 n) (j : P.B a i), r (f₀ i j) (f₁ i j)

theorem MvPFunctor.supp_eq {n : ℕ} {P : MvPFunctor.{u} n} {α : TypeVec.{u} n} (a : P.A) (f : (P.B a).Arrow α) (i : Fin2 n) : MvFunctor.supp ⟨a, f⟩ i = f i '' Set.univ

def MvPFunctor.drop {n : ℕ} (P : MvPFunctor.{u} (n + 1)) : MvPFunctor.{u} n

Split polynomial functor, get an n-ary functor from an n+1-ary functor

def MvPFunctor.last {n : ℕ} (P : MvPFunctor.{u} (n + 1)) : PFunctor.{u, u}

Split polynomial functor, get a univariate functor from an n+1-ary functor

@[reducible, inline]

abbrev MvPFunctor.appendContents {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u_1} n} {β : Type u_1} {a : P.A} (f' : (P.drop.B a).Arrow α) (f : P.last.B a → β) : (P.B a).Arrow (α ::: β)

append arrows of a polynomial functor application