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.

def MvQPF.Const (n : ) (A : Type u_1) (_v : TypeVec.{u} n) :
Type u_1

Constant multivariate functor

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

    Constructor for constant functor

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

      Destructor for constant functor

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

        map for constant functor

        Equations
        • x.map = x
        Instances For
          instance MvQPF.Const.MvFunctor {n : } {A : Type u} :
          Equations
          • MvQPF.Const.MvFunctor = { map := fun {α β : TypeVec.{?u.21} n} (_f : α.Arrow β) => MvQPF.Const.map }
          theorem MvQPF.Const.map_mk {n : } {A : Type u} {α : TypeVec.{u} n} {β : TypeVec.{u} n} (f : α.Arrow β) (x : A) :
          theorem MvQPF.Const.get_map {n : } {A : Type u} {α : TypeVec.{u} n} {β : TypeVec.{u} n} (f : α.Arrow β) (x : MvQPF.Const n A α) :
          (MvFunctor.map f x).get = x.get
          instance MvQPF.Const.mvqpf {n : } {A : Type u} :
          Equations
          • One or more equations did not get rendered due to their size.