Documentation

Mathlib.Data.QPF.Multivariate.Constructions.Sigma

Dependent product and sum of QPFs are QPFs #

source
def MvQPF.Sigma {n : ℕ} {A : Type u} (F : A → TypeVec n → Type u) (v : TypeVec n) :
Type u

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

Instances For
    source
    def MvQPF.Pi {n : ℕ} {A : Type u} (F : A → TypeVec n → Type u) (v : TypeVec n) :
    Type u

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

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

      polynomial functor representation of a dependent sum

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

            polynomial functor representation of a dependent product

            Instances For
              source
              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
                source
                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

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