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.
@[instance]
def
mvqpf.const.inhabited
(n : ℕ)
{A : Type u_1}
{α : typevec n}
[inhabited A] :
inhabited (mvqpf.const n A α)
Equations
- mvqpf.const.inhabited n = {default := inhabited.default A _inst_1}
Constructor for constant functor
Equations
- mvqpf.const.mk x = x
Destructor for constant functor
@[simp]
theorem
mvqpf.const.mk_get
{n : ℕ}
{A : Type u}
{α : typevec n}
(x : mvqpf.const n A α) :
mvqpf.const.mk x.get = x
@[simp]
theorem
mvqpf.const.get_mk
{n : ℕ}
{A : Type u}
{α : typevec n}
(x : A) :
(mvqpf.const.mk x).get = x
def
mvqpf.const.map
{n : ℕ}
{A : Type u}
{α β : typevec n} :
mvqpf.const n A α → mvqpf.const n A β
map for constant functor
Equations
- mvqpf.const.map = λ (x : mvqpf.const n A α), x
@[instance]
Equations
- mvqpf.const.mvfunctor = {map := λ (α β : typevec n) (f : α.arrow β), mvqpf.const.map}
theorem
mvqpf.const.map_mk
{n : ℕ}
{A : Type u}
{α β : typevec n}
(f : α.arrow β)
(x : A) :
mvfunctor.map f (mvqpf.const.mk x) = mvqpf.const.mk x
theorem
mvqpf.const.get_map
{n : ℕ}
{A : Type u}
{α β : typevec n}
(f : α.arrow β)
(x : mvqpf.const n A α) :
(mvfunctor.map f x).get = x.get
@[instance]
Equations
- mvqpf.const.mvqpf = {P := mvpfunctor.const n A, abs := λ (α : typevec n) (x : (mvpfunctor.const n A).obj α), mvpfunctor.const.get x, repr := λ (α : typevec n) (x : mvqpf.const n A α), mvpfunctor.const.mk n x, abs_repr := _, abs_map := _}