P — Mathlib · SciLib

English

There is a polynomial functor P for the projection that realizes the projection as a polynomial functor with components A and B depending on i. Specifically, A is a one-point type, and B_j is ULift of PLift of the equality i = j.

Русский

Для проекции существует полиномиальный функтор P, представляющий проекцию как полиномиального функторa: A состоит из одного элемента (единичное множество), а B_j равен ULift PLift(i = j).

LaTeX

$$$P : MvPFunctor n\\;\\text{ with } A := PUnit,\\; B_j := ULift\\\\ PLift (i = j).$$$

Lean4

/-- Polynomial representation of the projection functor -/
def P : MvPFunctor.{u} n where
  A := PUnit
  B _ j := ULift <| PLift <| i = j

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