Dependent product and sum of QPFs are QPFs

def MvQPF.Sigma {n : ℕ} {A : Type u} (F : A → TypeVec.{u} n → Type u) (v : TypeVec.{u} n) : Type u

Dependent sum of an n-ary functor. The sum can range over data types like ℕ or over Type.{u-1}

Equations

• MvQPF.Sigma F v = ((α : A) × F α v)

def MvQPF.Pi {n : ℕ} {A : Type u} (F : A → TypeVec.{u} n → Type u) (v : TypeVec.{u} n) : Type u

Dependent product of an n-ary functor. The sum can range over data types like ℕ or over Type.{u-1}

Equations

• MvQPF.Pi F v = ((α : A) → F α v)

instance MvQPF.Sigma.inhabited {n : ℕ} {A : Type u} (F : A → TypeVec.{u} n → Type u) {α : TypeVec.{u} n} [Inhabited A] [Inhabited (F default α)] : Inhabited (MvQPF.Sigma F α)

Equations

• MvQPF.Sigma.inhabited F = { default := ⟨default, default⟩ }

instance MvQPF.Pi.inhabited {n : ℕ} {A : Type u} (F : A → TypeVec.{u} n → Type u) {α : TypeVec.{u} n} [(a : A) → Inhabited (F a α)] : Inhabited (MvQPF.Pi F α)

Equations

• MvQPF.Pi.inhabited F = { default := fun (_a : A) => default }

instance MvQPF.Sigma.instMvFunctor {n : ℕ} {A : Type u} (F : A → TypeVec.{u} n → Type u) [(α : A) → MvFunctor (F α)] : MvFunctor (MvQPF.Sigma F)

Equations

• MvQPF.Sigma.instMvFunctor F = { map := fun {α β : TypeVec.{?u.42} n} (f : α.Arrow β) (x : MvQPF.Sigma F α) => match x with | ⟨a, x⟩ => ⟨a, MvFunctor.map f x⟩ }

def MvQPF.Sigma.P {n : ℕ} {A : Type u} (F : A → TypeVec.{u} n → Type u) [(α : A) → MvQPF (F α)] : MvPFunctor.{u} n

polynomial functor representation of a dependent sum

Equations

• MvQPF.Sigma.P F = { A := (a : A) × (MvQPF.P (F a)).A, B := fun (x : (a : A) × (MvQPF.P (F a)).A) => (MvQPF.P (F x.fst)).B x.snd }

def MvQPF.Sigma.abs {n : ℕ} {A : Type u} (F : A → TypeVec.{u} n → Type u) [(α : A) → MvQPF (F α)] ⦃α : TypeVec.{u} n⦄ : ↑(MvQPF.Sigma.P F) α → MvQPF.Sigma F α

abstraction function for dependent sums

Equations

• MvQPF.Sigma.abs F ⟨a, f⟩ = ⟨a.fst, MvQPF.abs ⟨a.snd, f⟩⟩

def MvQPF.Sigma.repr {n : ℕ} {A : Type u} (F : A → TypeVec.{u} n → Type u) [(α : A) → MvQPF (F α)] ⦃α : TypeVec.{u} n⦄ : MvQPF.Sigma F α → ↑(MvQPF.Sigma.P F) α

representation function for dependent sums

Equations

• MvQPF.Sigma.repr F ⟨a, x_1⟩ = ⟨⟨a, (MvQPF.repr x_1).fst⟩, (MvQPF.repr x_1).snd⟩

instance MvQPF.Sigma.inst {n : ℕ} {A : Type u} (F : A → TypeVec.{u} n → Type u) [(α : A) → MvQPF (F α)] : MvQPF (MvQPF.Sigma F)

Equations

• MvQPF.Sigma.inst F = MvQPF.mk (MvQPF.Sigma.P F) (fun {α : TypeVec.{?u.37} n} => MvQPF.Sigma.abs F) (fun {α : TypeVec.{?u.37} n} => MvQPF.Sigma.repr F) ⋯ ⋯

instance MvQPF.Pi.instMvFunctor {n : ℕ} {A : Type u} (F : A → TypeVec.{u} n → Type u) [(α : A) → MvFunctor (F α)] : MvFunctor (MvQPF.Pi F)

Equations

• MvQPF.Pi.instMvFunctor F = { map := fun {α β : TypeVec.{?u.39} n} (f : α.Arrow β) (x : MvQPF.Pi F α) (a : A) => MvFunctor.map f (x a) }

def MvQPF.Pi.P {n : ℕ} {A : Type u} (F : A → TypeVec.{u} n → Type u) [(α : A) → MvQPF (F α)] : MvPFunctor.{u} n

polynomial functor representation of a dependent product

Equations

• MvQPF.Pi.P F = { A := (a : A) → (MvQPF.P (F a)).A, B := fun (x : (a : A) → (MvQPF.P (F a)).A) (i : Fin2 n) => (a : A) × (MvQPF.P (F a)).B (x a) i }

def MvQPF.Pi.abs {n : ℕ} {A : Type u} (F : A → TypeVec.{u} n → Type u) [(α : A) → MvQPF (F α)] ⦃α : TypeVec.{u} n⦄ : ↑(MvQPF.Pi.P F) α → MvQPF.Pi F α

abstraction function for dependent products

Equations

• MvQPF.Pi.abs F ⟨a, f⟩ = fun (x : A) => MvQPF.abs ⟨a x, fun (i : Fin2 n) (y : (MvQPF.P (F x)).B (a x) i) => f i ⟨x, y⟩⟩

def MvQPF.Pi.repr {n : ℕ} {A : Type u} (F : A → TypeVec.{u} n → Type u) [(α : A) → MvQPF (F α)] ⦃α : TypeVec.{u} n⦄ : MvQPF.Pi F α → ↑(MvQPF.Pi.P F) α

representation function for dependent products

Equations

• MvQPF.Pi.repr F x = ⟨fun (a : A) => (MvQPF.repr (x a)).fst, fun (_i : Fin2 n) (a : (MvQPF.Pi.P F).B (fun (a : A) => (MvQPF.repr (x a)).fst) _i) => (MvQPF.repr (x a.fst)).snd _i a.snd⟩

instance MvQPF.Pi.inst {n : ℕ} {A : Type u} (F : A → TypeVec.{u} n → Type u) [(α : A) → MvQPF (F α)] : MvQPF (MvQPF.Pi F)

Equations

• MvQPF.Pi.inst F = MvQPF.mk (MvQPF.Pi.P F) (MvQPF.Pi.abs F) (MvQPF.Pi.repr F) ⋯ ⋯