Documentation

Mathlib.Data.QPF.Multivariate.Constructions.Sigma

Dependent product and sum of QPFs are QPFs #

def MvQPF.Sigma {n : } {A : Type u} (F : ATypeVec nType u) (v : TypeVec n) :

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 : ATypeVec nType u) (v : TypeVec n) :

    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 : ATypeVec nType u) {α : TypeVec n} [Inhabited A] [Inhabited (F default α)] :
      instance MvQPF.Pi.inhabited {n : } {A : Type u} (F : ATypeVec nType u) {α : TypeVec n} [(a : A) → Inhabited (F a α)] :
      instance MvQPF.Sigma.instMvFunctorSigma {n : } {A : Type u} (F : ATypeVec nType u) [(α : A) → MvFunctor (F α)] :
      def MvQPF.Sigma.P {n : } {A : Type u} (F : ATypeVec nType 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 : ATypeVec nType u) [(α : A) → MvFunctor (F α)] [(α : A) → MvQPF (F α)] ⦃α : TypeVec n :

        abstraction function for dependent sums

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

          representation function for dependent sums

          Instances For
            instance MvQPF.Sigma.instMvQPFSigmaInstMvFunctorSigma {n : } {A : Type u} (F : ATypeVec nType u) [(α : A) → MvFunctor (F α)] [(α : A) → MvQPF (F α)] :
            instance MvQPF.Pi.instMvFunctorPi {n : } {A : Type u} (F : ATypeVec nType u) [(α : A) → MvFunctor (F α)] :
            def MvQPF.Pi.P {n : } {A : Type u} (F : ATypeVec nType 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 : ATypeVec nType u) [(α : A) → MvFunctor (F α)] [(α : A) → MvQPF (F α)] ⦃α : TypeVec n :

              abstraction function for dependent products

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

                representation function for dependent products

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