mathlib documentation

data.qpf.multivariate.constructions.sigma

Dependent product and sum of QPFs are QPFs #

def mvqpf.sigma {n : } {A : Type u} (F : A → typevec nType u) (v : typevec n) :
Type u

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

Equations
Instances for mvqpf.sigma
def mvqpf.pi {n : } {A : Type u} (F : A → typevec nType u) (v : typevec n) :
Type u

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

Equations
Instances for mvqpf.pi
@[protected, instance]
def mvqpf.sigma.inhabited {n : } {A : Type u} (F : A → typevec nType u) {α : typevec n} [inhabited A] [inhabited (F inhabited.default α)] :
Equations
@[protected, instance]
def mvqpf.pi.inhabited {n : } {A : Type u} (F : A → typevec nType u) {α : typevec n} [Π (a : A), inhabited (F a α)] :
Equations
@[protected, instance]
def mvqpf.sigma.mvfunctor {n : } {A : Type u} (F : A → typevec nType u) [Π (α : A), mvfunctor (F α)] :
Equations
@[protected]
def mvqpf.sigma.P {n : } {A : Type u} (F : A → typevec nType u) [Π (α : A), mvfunctor (F α)] [Π (α : A), mvqpf (F α)] :

polynomial functor representation of a dependent sum

Equations
@[protected]
def mvqpf.sigma.abs {n : } {A : Type u} (F : A → typevec nType u) [Π (α : A), mvfunctor (F α)] [Π (α : A), mvqpf (F α)] ⦃α : typevec n⦄ :
(mvqpf.sigma.P F).obj αmvqpf.sigma F α

abstraction function for dependent sums

Equations
@[protected]
def mvqpf.sigma.repr {n : } {A : Type u} (F : A → typevec nType u) [Π (α : A), mvfunctor (F α)] [Π (α : A), mvqpf (F α)] ⦃α : typevec n⦄ :
mvqpf.sigma F α(mvqpf.sigma.P F).obj α

representation function for dependent sums

Equations
@[protected, instance]
def mvqpf.sigma.mvqpf {n : } {A : Type u} (F : A → typevec nType u) [Π (α : A), mvfunctor (F α)] [Π (α : A), mvqpf (F α)] :
Equations
@[protected, instance]
def mvqpf.pi.mvfunctor {n : } {A : Type u} (F : A → typevec nType u) [Π (α : A), mvfunctor (F α)] :
Equations
@[protected]
def mvqpf.pi.P {n : } {A : Type u} (F : A → typevec nType u) [Π (α : A), mvfunctor (F α)] [Π (α : A), mvqpf (F α)] :

polynomial functor representation of a dependent product

Equations
@[protected]
def mvqpf.pi.abs {n : } {A : Type u} (F : A → typevec nType u) [Π (α : A), mvfunctor (F α)] [Π (α : A), mvqpf (F α)] ⦃α : typevec n⦄ :
(mvqpf.pi.P F).obj αmvqpf.pi F α

abstraction function for dependent products

Equations
@[protected]
def mvqpf.pi.repr {n : } {A : Type u} (F : A → typevec nType u) [Π (α : A), mvfunctor (F α)] [Π (α : A), mvqpf (F α)] ⦃α : typevec n⦄ :
mvqpf.pi F α(mvqpf.pi.P F).obj α

representation function for dependent products

Equations
@[protected, instance]
def mvqpf.pi.mvqpf {n : } {A : Type u} (F : A → typevec nType u) [Π (α : A), mvfunctor (F α)] [Π (α : A), mvqpf (F α)] :
Equations