Documentation

Mathlib.Data.QPF.Multivariate.Constructions.Sigma

Dependent product and sum of QPFs are QPFs #

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

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

Equations
Instances For
    def MvQPF.Pi {n : } {A : Type u} (F : ATypeVec.{u} nType u) (v : TypeVec.{u} n) :

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

      polynomial functor representation of a dependent sum

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

        abstraction function for dependent sums

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

          representation function for dependent sums

          Equations
          Instances For
            instance MvQPF.Sigma.inst {n : } {A : Type u} (F : ATypeVec.{u} nType u) [(α : A) → MvQPF (F α)] :
            Equations
            instance MvQPF.Pi.instMvFunctor {n : } {A : Type u} (F : ATypeVec.{u} nType u) [(α : A) → MvFunctor (F α)] :
            Equations
            def MvQPF.Pi.P {n : } {A : Type u} (F : ATypeVec.{u} nType u) [(α : A) → MvQPF (F α)] :

            polynomial functor representation of a dependent product

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

              abstraction function for dependent products

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

                representation function for dependent products

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