instCoeFunForallTypeVecType — Mathlib

English

There is a canonical way to view a multivariate functor as a functor-valued function, i.e., a CoeFun instance pushing P.Obj to TypeVec n → Type.

Русский

Существует канонический способ рассматривать многопеременный функтор как функцию-объект, т.е. как экземпляр CoeFun: P.Obj → (TypeVec n → Type).

LaTeX

$$$$ \\text{There exists a canonical coercion } P : MvPFunctor(n) \\to (TypeVec(n) \\to Type) \\text{ given by } \\alpha \\mapsto \\mathrm{Obj}_P(\\alpha). $$$$

Lean4

instance : CoeFun (MvPFunctor.{u} n) (fun _ => TypeVec.{u} n → Type u) where coe := Obj

Похожие утверждения