Theorems · Inductive type · category theory

PFunctor

Type (max (uA + 1) (uB + 1))

A polynomial functor P is given by a type A and a family B of types over A. P maps any type α to a new type P α, which is defined as the sigma type Σ x, P.B x → α. An element of P α is a pair ⟨a, f⟩, where a is an element of a type A and f : B a → α. Think of a as the shape of the object and f as an index to the relevant elements of α.

Defined in

Mathlib.Data.PFunctor.Univariate.Basic

Cited by

75 results in Mathlib

Foundations

Depth 0 from the axioms · uses no axioms