mathlib documentation

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.

@[nolint]
def mvqpf.const (n : ) (A : Type u_1) (v : typevec n) :
Type u_1

Constant multivariate functor

Equations
Instances for mvqpf.const
@[protected, instance]
def mvqpf.const.inhabited (n : ) {A : Type u_1} {α : typevec n} [inhabited A] :
Equations
@[protected]
def mvqpf.const.mk {n : } {A : Type u} {α : typevec n} (x : A) :

Constructor for constant functor

Equations
@[protected]
def mvqpf.const.get {n : } {A : Type u} {α : typevec n} (x : mvqpf.const n A α) :
A

Destructor for constant functor

Equations
@[protected, simp]
theorem mvqpf.const.mk_get {n : } {A : Type u} {α : typevec n} (x : mvqpf.const n A α) :
@[protected, simp]
theorem mvqpf.const.get_mk {n : } {A : Type u} {α : typevec n} (x : A) :
@[protected]
def mvqpf.const.map {n : } {A : Type u} {α β : typevec n} :
mvqpf.const n A αmvqpf.const n A β

map for constant functor

Equations
@[protected, instance]
def mvqpf.const.mvfunctor {n : } {A : Type u} :
Equations
theorem mvqpf.const.map_mk {n : } {A : Type u} {α β : typevec n} (f : α.arrow β) (x : A) :
theorem mvqpf.const.get_map {n : } {A : Type u} {α β : typevec n} (f : α.arrow β) (x : mvqpf.const n A α) :
@[protected, instance]
def mvqpf.const.mvqpf {n : } {A : Type u} :
Equations