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.{u} n → Type u) (v : TypeVec.{u} n) :
Type u

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

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

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

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

                polynomial functor representation of a dependent sum

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

                    abstraction function for dependent sums

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

                        representation function for dependent sums

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

                                polynomial functor representation of a dependent product

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

                                    abstraction function for dependent products

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

                                        representation function for dependent products

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