Dependent product and sum of QPFs are QPFs #
instance
MvQPF.Sigma.instMvFunctorSigma
{n : ℕ}
{A : Type u}
(F : A → TypeVec n → Type u)
[(α : A) → MvFunctor (F α)]
:
MvFunctor (MvQPF.Sigma F)
def
MvQPF.Sigma.abs
{n : ℕ}
{A : Type u}
(F : A → TypeVec n → Type u)
[(α : A) → MvFunctor (F α)]
[(α : A) → MvQPF (F α)]
⦃α : TypeVec n⦄
:
MvPFunctor.Obj (MvQPF.Sigma.P F) α → MvQPF.Sigma F α
abstraction function for dependent sums
Instances For
def
MvQPF.Sigma.repr
{n : ℕ}
{A : Type u}
(F : A → TypeVec n → Type u)
[(α : A) → MvFunctor (F α)]
[(α : A) → MvQPF (F α)]
⦃α : TypeVec n⦄
:
MvQPF.Sigma F α → MvPFunctor.Obj (MvQPF.Sigma.P F) α
representation function for dependent sums
Instances For
instance
MvQPF.Sigma.instMvQPFSigmaInstMvFunctorSigma
{n : ℕ}
{A : Type u}
(F : A → TypeVec n → Type u)
[(α : A) → MvFunctor (F α)]
[(α : A) → MvQPF (F α)]
:
MvQPF (MvQPF.Sigma F)
def
MvQPF.Pi.abs
{n : ℕ}
{A : Type u}
(F : A → TypeVec n → Type u)
[(α : A) → MvFunctor (F α)]
[(α : A) → MvQPF (F α)]
⦃α : TypeVec n⦄
:
MvPFunctor.Obj (MvQPF.Pi.P F) α → MvQPF.Pi F α
abstraction function for dependent products
Instances For
def
MvQPF.Pi.repr
{n : ℕ}
{A : Type u}
(F : A → TypeVec n → Type u)
[(α : A) → MvFunctor (F α)]
[(α : A) → MvQPF (F α)]
⦃α : TypeVec n⦄
:
MvQPF.Pi F α → MvPFunctor.Obj (MvQPF.Pi.P F) α
representation function for dependent products