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 : TypeVec.{u} n) : Type u_1

Constant multivariate functor

Equations

• MvQPF.Const n A _v = A

instance MvQPF.Const.inhabited (n : ℕ) {A : Type u_1} {α : TypeVec.{u_2} n} [Inhabited A] : Inhabited (MvQPF.Const n A α)

Equations

• MvQPF.Const.inhabited n = { default := default }

def MvQPF.Const.mk {n : ℕ} {A : Type u} {α : TypeVec.{u} n} (x : A) : MvQPF.Const n A α

Constructor for constant functor

Equations

• MvQPF.Const.mk x = x

def MvQPF.Const.get {n : ℕ} {A : Type u} {α : TypeVec.{u} n} (x : MvQPF.Const n A α) : A

Destructor for constant functor

Equations

• x.get = x

@[simp]

theorem MvQPF.Const.mk_get {n : ℕ} {A : Type u} {α : TypeVec.{u} n} (x : MvQPF.Const n A α) : MvQPF.Const.mk x.get = x

@[simp]

theorem MvQPF.Const.get_mk {n : ℕ} {A : Type u} {α : TypeVec.{u} n} (x : A) : (MvQPF.Const.mk x).get = x

def MvQPF.Const.map {n : ℕ} {A : Type u} {α : TypeVec.{u} n} {β : TypeVec.{u} n} : MvQPF.Const n A α → MvQPF.Const n A β

map for constant functor

Equations

• x.map = x

instance MvQPF.Const.MvFunctor {n : ℕ} {A : Type u} : MvFunctor (MvQPF.Const n A)

Equations

• MvQPF.Const.MvFunctor = { map := fun {α β : TypeVec.{?u.21} n} (_f : α.Arrow β) => MvQPF.Const.map }

theorem MvQPF.Const.map_mk {n : ℕ} {A : Type u} {α : TypeVec.{u} n} {β : TypeVec.{u} 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.{u} n} {β : TypeVec.{u} n} (f : α.Arrow β) (x : MvQPF.Const n A α) : (MvFunctor.map f x).get = x.get

instance MvQPF.Const.mvqpf {n : ℕ} {A : Type u} : MvQPF (MvQPF.Const n A)

Equations

• One or more equations did not get rendered due to their size.