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 := { fst := default, snd := 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.instMvFunctorSigma {n : ℕ} {A : Type u} (F : A → TypeVec.{u} n → Type u) [(α : A) → MvFunctor (F α)] : MvFunctor (MvQPF.Sigma F)

Equations

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

def MvQPF.Sigma.P {n : ℕ} {A : Type u} (F : A → TypeVec.{u} n → Type u) [(α : A) → MvFunctor (F α)] [(α : 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) → MvFunctor (F α)] [(α : A) → MvQPF (F α)] ⦃α : TypeVec.{u} n⦄ : ↑(MvQPF.Sigma.P F) α → MvQPF.Sigma F α

abstraction function for dependent sums

Equations

• MvQPF.Sigma.abs F x = match x with | { fst := a, snd := f } => { fst := a.fst, snd := MvQPF.abs { fst := a.snd, snd := f } }

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

representation function for dependent sums

Equations

• MvQPF.Sigma.repr F x = match x with | { fst := a, snd := f } => let x := MvQPF.repr f; { fst := { fst := a, snd := x.fst }, snd := x.snd }

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

Equations

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

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

Equations

• MvQPF.Pi.instMvFunctorPi F = { map := fun {α β : TypeVec.{u} n} (f : TypeVec.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) → MvFunctor (F α)] [(α : 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) → MvFunctor (F α)] [(α : A) → MvQPF (F α)] ⦃α : TypeVec.{u} n⦄ : ↑(MvQPF.Pi.P F) α → MvQPF.Pi F α

abstraction function for dependent products

Equations

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

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

representation function for dependent products

Equations

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

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

Equations

• MvQPF.Pi.instMvQPFPiInstMvFunctorPi F = { P := MvQPF.Pi.P F, abs := MvQPF.Pi.abs F, repr := MvQPF.Pi.repr F, abs_repr := ⋯, abs_map := ⋯ }