# Documentation

Mathlib.Data.QPF.Multivariate.Constructions.Sigma

# 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}

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}

Instances For
instance MvQPF.Sigma.inhabited {n : } {A : Type u} (F : AType u) {α : } [] [Inhabited (F default α)] :
instance MvQPF.Pi.inhabited {n : } {A : Type u} (F : AType u) {α : } [(a : A) → Inhabited (F a α)] :
instance MvQPF.Sigma.instMvFunctorSigma {n : } {A : Type u} (F : AType u) [(α : A) → MvFunctor (F α)] :
def MvQPF.Sigma.P {n : } {A : Type u} (F : AType u) [(α : A) → MvFunctor (F α)] [(α : A) → MvQPF (F α)] :

polynomial functor representation of a dependent sum

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

abstraction function for dependent sums

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

representation function for dependent sums

Instances For
instance MvQPF.Sigma.instMvQPFSigmaInstMvFunctorSigma {n : } {A : Type u} (F : AType u) [(α : A) → MvFunctor (F α)] [(α : A) → MvQPF (F α)] :
instance MvQPF.Pi.instMvFunctorPi {n : } {A : Type u} (F : AType u) [(α : A) → MvFunctor (F α)] :
def MvQPF.Pi.P {n : } {A : Type u} (F : AType u) [(α : A) → MvFunctor (F α)] [(α : A) → MvQPF (F α)] :

polynomial functor representation of a dependent product

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

abstraction function for dependent products

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

representation function for dependent products

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