Constant functors are QPFs #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.
@[protected, 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 _inst_1}
@[protected]
Destructor for constant functor
@[protected, simp]
theorem
mvqpf.const.mk_get
{n : ℕ}
{A : Type u}
{α : typevec n}
(x : mvqpf.const n A α) :
mvqpf.const.mk x.get = x
@[protected, simp]
theorem
mvqpf.const.get_mk
{n : ℕ}
{A : Type u}
{α : typevec n}
(x : A) :
(mvqpf.const.mk x).get = x
@[protected, 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
@[protected, 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 := _}