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

Equations

• ↑P α = ((a : P.A) × (P.B a).Arrow α)

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

Equations

• MvPFunctor.instCoeFunForallTypeVecType = { coe := MvPFunctor.Obj }

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

Applying P to a morphism of Type

Equations

• P.map f x = match x with | ⟨a, g⟩ => ⟨a, TypeVec.comp f g⟩

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

Equations

• MvPFunctor.instInhabited = { default := { A := default, B := default } }

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

Equations

• MvPFunctor.Obj.inhabited P = { default := ⟨default, fun (x : Fin2 n) (x_1 : P.B default x) => default⟩ }

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

Equations

• P.instMvFunctorObj = { map := @MvPFunctor.map n P }

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

Equations

• ⋯ = ⋯

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

Constant functor where the input object does not affect the output

Equations

• MvPFunctor.const n A = { A := A, B := fun (x : A) (x : Fin2 n) => PEmpty.{u + 1} }

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

Constructor for the constant functor

Equations

• MvPFunctor.const.mk n x = ⟨x, fun (x_1 : Fin2 n) (a : (MvPFunctor.const n A).B x x_1) => PEmpty.elim a⟩

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

Destructor for the constant functor

Equations

• MvPFunctor.const.get x = x.fst

@[simp]

theorem MvPFunctor.const.get_map {n : ℕ} {A : Type u} {α : TypeVec.{u} n} {β : TypeVec.{u} n} (f : α.Arrow β) (x : ↑(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.{u} n} (x : A) : MvPFunctor.const.get (MvPFunctor.const.mk n x) = x

@[simp]

theorem MvPFunctor.const.mk_get {n : ℕ} {A : Type u} {α : TypeVec.{u} n} (x : ↑(MvPFunctor.const n A) α) : MvPFunctor.const.mk n (MvPFunctor.const.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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• MvPFunctor.comp.get x = ⟨x.fst.fst, fun (i : Fin2 n) (a : P.B x.fst.fst i) => ⟨x.fst.snd i a, fun (j : Fin2 m) (b : (Q i).B (x.fst.snd i a) j) => x.snd j ⟨i, ⟨a, b⟩⟩⟩⟩

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

Equations

• P.drop = { A := P.A, B := fun (a : P.A) => (P.B a).drop }

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

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

Equations

• P.last = { A := P.A, B := fun (a : P.A) => (P.B a).last }

@[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

Equations

• P.appendContents f' f = TypeVec.splitFun f' f