Dependent product and sum of QPFs are QPFs #

def MvQPF.Sigma {n : } {A : Type u} (F : AType u) (v : ) :

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

Equations
• = ((α : A) × F α v)
Instances For
def MvQPF.Pi {n : } {A : Type u} (F : AType u) (v : ) :

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

Equations
Instances For
instance MvQPF.Sigma.inhabited {n : } {A : Type u} (F : AType u) {α : } [] [Inhabited (F default α)] :
Equations
• = { default := default, default }
instance MvQPF.Pi.inhabited {n : } {A : Type u} (F : AType u) {α : } [(a : A) → Inhabited (F a α)] :
Equations
• = { default := fun (_a : A) => default }
instance MvQPF.Sigma.instMvFunctor {n : } {A : Type u} (F : AType u) [(α : A) → MvFunctor (F α)] :
Equations
• = { map := fun {α β : } (f : α.Arrow β) (x : ) => match x with | a, x => a, ⟩ }
def MvQPF.Sigma.P {n : } {A : Type u} (F : AType u) [(α : A) → MvQPF (F α)] :

polynomial functor representation of a dependent sum

Equations
• = { 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 }
Instances For
def MvQPF.Sigma.abs {n : } {A : Type u} (F : AType u) [(α : A) → MvQPF (F α)] ⦃α : :
α

abstraction function for dependent sums

Equations
Instances For
def MvQPF.Sigma.repr {n : } {A : Type u} (F : AType u) [(α : A) → MvQPF (F α)] ⦃α : :
α

representation function for dependent sums

Equations
Instances For
instance MvQPF.Sigma.inst {n : } {A : Type u} (F : AType u) [(α : A) → MvQPF (F α)] :
Equations
• = MvQPF.mk (fun {α : } => ) (fun {α : } => )
instance MvQPF.Pi.instMvFunctor {n : } {A : Type u} (F : AType u) [(α : A) → MvFunctor (F α)] :
Equations
def MvQPF.Pi.P {n : } {A : Type u} (F : AType u) [(α : A) → MvQPF (F α)] :

polynomial functor representation of a dependent product

Equations
• = { 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 }
Instances For
def MvQPF.Pi.abs {n : } {A : Type u} (F : AType u) [(α : A) → MvQPF (F α)] ⦃α : :
(MvQPF.Pi.P F) αMvQPF.Pi F α

abstraction function for dependent products

Equations
Instances For
def MvQPF.Pi.repr {n : } {A : Type u} (F : AType u) [(α : A) → MvQPF (F α)] ⦃α : :
MvQPF.Pi F α(MvQPF.Pi.P F) α

representation function for dependent products

Equations
Instances For
instance MvQPF.Pi.inst {n : } {A : Type u} (F : AType u) [(α : A) → MvQPF (F α)] :
Equations