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)

• A : Type u

  The head type

• B : s.A → TypeVec n

  The child family of types

multivariate polynomial functors

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

Applying P to an object of Type

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

Applying P to a morphism of Type

instance MvPFunctor.instInhabitedMvPFunctor {n : ℕ} : Inhabited (MvPFunctor n)

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

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

theorem MvPFunctor.map_eq {n : ℕ} (P : MvPFunctor n) {α : TypeVec n} {β : TypeVec n} (g : TypeVec.Arrow α β) (a : P.A) (f : TypeVec.Arrow (MvPFunctor.B P a) α) : MvFunctor.map g { fst := a, snd := f } = { fst := a, snd := TypeVec.comp g f }

theorem MvPFunctor.id_map {n : ℕ} (P : MvPFunctor n) {α : TypeVec n} (x : MvPFunctor.Obj P α) : MvFunctor.map TypeVec.id x = x

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

instance MvPFunctor.instLawfulMvFunctorObjInstMvFunctorObj {n : ℕ} (P : MvPFunctor n) : LawfulMvFunctor (MvPFunctor.Obj P)

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

Constant functor where the input object does not affect the output

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

Constructor for the constant functor

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

Destructor for the constant functor

@[simp]

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

@[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.Obj (MvPFunctor.const n A) α) : MvPFunctor.const.mk n (MvPFunctor.const.get x) = x

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

Functor composition on polynomial functors

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

Constructor for functor composition

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

Destructor for functor composition

theorem MvPFunctor.comp.get_map {n : ℕ} {m : ℕ} {P : MvPFunctor n} {Q : Fin2 n → MvPFunctor m} {α : TypeVec m} {β : TypeVec m} (f : TypeVec.Arrow α β) (x : MvPFunctor.Obj (MvPFunctor.comp P Q) α) : MvPFunctor.comp.get (MvFunctor.map f x) = MvFunctor.map (fun i x => 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 : MvPFunctor.Obj P fun i => MvPFunctor.Obj (Q i) α) : MvPFunctor.comp.get (MvPFunctor.comp.mk x) = x

@[simp]

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

theorem MvPFunctor.liftP_iff {n : ℕ} {P : MvPFunctor n} {α : TypeVec n} (p : ⦃i : Fin2 n⦄ → α i → Prop) (x : MvPFunctor.Obj P α) : MvFunctor.LiftP p x ↔ ∃ a f, x = { fst := a, snd := f } ∧ ((i : Fin2 n) → (j : MvPFunctor.B P a i) → p i (f i j))

theorem MvPFunctor.liftP_iff' {n : ℕ} {P : MvPFunctor n} {α : TypeVec n} (p : ⦃i : Fin2 n⦄ → α i → Prop) (a : P.A) (f : TypeVec.Arrow (MvPFunctor.B P a) α) : MvFunctor.LiftP p { fst := a, snd := f } ↔ (i : Fin2 n) → (x : MvPFunctor.B P a i) → p i (f i x)

theorem MvPFunctor.liftR_iff {n : ℕ} {P : MvPFunctor n} {α : TypeVec n} (r : ⦃i : Fin2 n⦄ → α i → α i → Prop) (x : MvPFunctor.Obj P α) (y : MvPFunctor.Obj P α) : MvFunctor.LiftR r x y ↔ ∃ a f₀ f₁, x = { fst := a, snd := f₀ } ∧ y = { fst := a, snd := f₁ } ∧ ((i : Fin2 n) → (j : MvPFunctor.B P a i) → r i (f₀ i j) (f₁ i j))

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

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

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

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

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

@[reducible]

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

append arrows of a polynomial functor application