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_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

• MvQPF.Sigma.instMvFunctor F = { map := fun {α β : TypeVec.{?u.1} 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⦄ : ↑(Sigma.P F) α → 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⦄ : Sigma F α → ↑(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_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

• MvQPF.Pi.instMvFunctor F = { map := fun {α β : TypeVec.{?u.1} 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⦄ : ↑(Pi.P F) α → 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⦄ : Pi F α → ↑(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_reducible]

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

Equations

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