# 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 : ) :
Type u_1

Constant multivariate functor

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

Constructor for constant functor

Equations
Instances For
def MvQPF.Const.get {n : } {A : Type u} {α : } (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} {α : } (x : MvQPF.Const n A α) :
@[simp]
theorem MvQPF.Const.get_mk {n : } {A : Type u} {α : } (x : A) :
().get = x
def MvQPF.Const.map {n : } {A : Type u} {α : } {β : } :
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 {α β : } (_f : α.Arrow β) => MvQPF.Const.map }
theorem MvQPF.Const.map_mk {n : } {A : Type u} {α : } {β : } (f : α.Arrow β) (x : A) :
theorem MvQPF.Const.get_map {n : } {A : Type u} {α : } {β : } (f : α.Arrow β) (x : MvQPF.Const n A α) :
().get = x.get
instance MvQPF.Const.mvqpf {n : } {A : Type u} :
Equations
• One or more equations did not get rendered due to their size.