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

Constant multivariate functor

Equations
@[instance]
def mvqpf.const.inhabited (n : ) {A : Type u_1} {α : typevec n} [inhabited A] :

Equations
def mvqpf.const.mk {n : } {A : Type u} {α : typevec n} :
A → mvqpf.const n A α

Constructor for constant functor

Equations
def mvqpf.const.get {n : } {A : Type u} {α : typevec n} :
mvqpf.const n A α → A

Destructor for constant functor

Equations
@[simp]
theorem mvqpf.const.mk_get {n : } {A : Type u} {α : typevec n} (x : mvqpf.const n A α) :

@[simp]
theorem mvqpf.const.get_mk {n : } {A : Type u} {α : typevec n} (x : A) :

def mvqpf.const.map {n : } {A : Type u} {α β : typevec n} :
mvqpf.const n A αmvqpf.const n A β

map for constant functor

Equations
@[instance]
def mvqpf.const.mvfunctor {n : } {A : Type u} :

Equations
theorem mvqpf.const.map_mk {n : } {A : Type u} {α β : typevec n} (f : α β) (x : A) :

theorem mvqpf.const.get_map {n : } {A : Type u} {α β : typevec n} (f : α β) (x : mvqpf.const n A α) :
(f <$$> x).get = x.get

@[instance]
def mvqpf.const.mvqpf {n : } {A : Type u} :

Equations