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) × TypeVec.Arrow (P.B a) α)

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

Equations

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

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

Applying P to a morphism of Type

Equations

• MvPFunctor.map P f x = match x with | { fst := a, snd := g } => { fst := a, snd := TypeVec.comp f g }

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

Equations

• MvPFunctor.instInhabitedMvPFunctor = { 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 := { fst := default, snd := fun (x : Fin2 n) (x_1 : P.B default x) => default } }

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

Equations

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

theorem MvPFunctor.map_eq {n : ℕ} (P : MvPFunctor.{u} n) {α : TypeVec.{u} n} {β : TypeVec.{u} n} (g : TypeVec.Arrow α β) (a : P.A) (f : TypeVec.Arrow (P.B a) α) : MvFunctor.map g { fst := a, snd := f } = { fst := a, snd := 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 : TypeVec.Arrow α β) (g : TypeVec.Arrow β γ) (x : ↑P α) : MvFunctor.map (TypeVec.comp g f) x = MvFunctor.map g (MvFunctor.map f x)

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

Equations

• (_ : LawfulMvFunctor ↑P) = (_ : LawfulMvFunctor ↑P)

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 = { fst := x, snd := 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 : TypeVec.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) α) : ↑(MvPFunctor.comp P 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 : ↑(MvPFunctor.comp P Q) α) : ↑P fun (i : Fin2 n) => ↑(Q i) α

Destructor for functor composition

Equations

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

theorem MvPFunctor.comp.get_map {n : ℕ} {m : ℕ} {P : MvPFunctor.{u} n} {Q : Fin2 n → MvPFunctor.{u} m} {α : TypeVec.{u} m} {β : TypeVec.{u} m} (f : TypeVec.Arrow α β) (x : ↑(MvPFunctor.comp P 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 : ↑(MvPFunctor.comp P 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 : TypeVec.Arrow (P.B a) α), x = { fst := a, snd := 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 : TypeVec.Arrow (P.B a) α) : MvFunctor.LiftP p { fst := a, snd := 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₀ : TypeVec.Arrow (P.B a) α) (f₁ : TypeVec.Arrow (P.B a) α), x = { fst := a, snd := f₀ } ∧ y = { fst := a, snd := 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 : TypeVec.Arrow (P.B a) α) (i : Fin2 n) : MvFunctor.supp { fst := a, snd := 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

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

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

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

@[reducible]

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

append arrows of a polynomial functor application

Equations

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