Documentation

Mathlib.Data.QPF.Multivariate.Constructions.Const

Constant functors are QPFs #

Constant functors map every type vectors to the same target type. This is a useful device for constructing data types from more basic types that are not actually functorial. For instance Const n Nat makes Nat into a functor that can be used in a functor-based data type specification.

source
def MvQPF.Const (n : ℕ) (A : Type u_1) (_v : TypeVec n) :
Type u_1

Constant multivariate functor

Instances For
    source
    instance MvQPF.Const.inhabited (n : ℕ) {A : Type u_1} {α : TypeVec n} [Inhabited A] :
    Inhabited (MvQPF.Const n A α)
    source
    def MvQPF.Const.mk {n : ℕ} {A : Type u} {α : TypeVec n} (x : A) :
    MvQPF.Const n A α

    Constructor for constant functor

    Instances For
      source
      def MvQPF.Const.get {n : ℕ} {A : Type u} {α : TypeVec n} (x : MvQPF.Const n A α) :
      A

      Destructor for constant functor

      Instances For
        source
        @[simp]
        theorem MvQPF.Const.mk_get {n : ℕ} {A : Type u} {α : TypeVec n} (x : MvQPF.Const n A α) :
        MvQPF.Const.mk (MvQPF.Const.get x) = x
        source
        @[simp]
        theorem MvQPF.Const.get_mk {n : ℕ} {A : Type u} {α : TypeVec n} (x : A) :
        MvQPF.Const.get (MvQPF.Const.mk x) = x
        source
        def MvQPF.Const.map {n : ℕ} {A : Type u} {α : TypeVec n} {β : TypeVec n} :
        MvQPF.Const n A α → MvQPF.Const n A β

        map for constant functor

        Instances For
          source
          instance MvQPF.Const.MvFunctor {n : ℕ} {A : Type u} :
          MvFunctor (MvQPF.Const n A)
          source
          theorem MvQPF.Const.map_mk {n : ℕ} {A : Type u} {α : TypeVec n} {β : TypeVec n} (f : TypeVec.Arrow α β) (x : A) :
          MvFunctor.map f (MvQPF.Const.mk x) = MvQPF.Const.mk x
          source
          theorem MvQPF.Const.get_map {n : ℕ} {A : Type u} {α : TypeVec n} {β : TypeVec n} (f : TypeVec.Arrow α β) (x : MvQPF.Const n A α) :
          MvQPF.Const.get (MvFunctor.map f x) = MvQPF.Const.get x
          source
          instance MvQPF.Const.mvqpf {n : ℕ} {A : Type u} :
          MvQPF (MvQPF.Const n A)