Polynomial Functors, Lens, and Charts

This file defines polynomial functors, lenses, and charts. The goal is to provide basic definitions, with their properties and categories defined in later files.

dt: this file is getting long and should maybe be split up more.

@[instance_reducible]

instance PFunctor.instZeroPFunctor : Zero PFunctor.{uA, uB}

The zero polynomial functor, defined as A = PEmpty and B _ = PEmpty, is the identity with respect to sum (up to equivalence)

@[instance_reducible]

instance PFunctor.instOnePFunctor : One PFunctor.{uA, uB}

The unit polynomial functor, defined as A = PUnit and B _ = PEmpty, is the identity with respect to product (up to equivalence)

def PFunctor.y : PFunctor.{uA, uB}

The variable (or identity) polynomial functor y, with a single position and a single direction. Under the Yoneda reading y = y^ PUnit is the representable on a point; it is the unit for both composition ◃ and the tensor product ⊗ (up to equivalence).

@[deprecated PFunctor.y (since := "2026-08-17")]

def PFunctor.X : PFunctor.{uA, uB}

Deprecated compatibility name for the variable polynomial.

instance PFunctor.instIsEmptyAOfNat_polyFun : IsEmpty (A 0)

@[instance_reducible]

instance PFunctor.instUniqueAOfNatOne : Unique (A 1)

@[instance_reducible]

instance PFunctor.instUniqueAY : Unique y.A

def PFunctor.monomial (A : Type uA) (B : Type uB) : PFunctor.{uA, uB}

The monomial functor A y^ B has A as its head type and the constant family B_a = B as the child type for each each shape a : A .

def PFunctor.«term_Y^_» : Lean.TrailingParserDescr

The monomial functor A y^ B has A as its head type and the constant family B_a = B as the child type for each each shape a : A .

def PFunctor.«term_X^_» : Lean.TrailingParserDescr

Parse-only compatibility spelling of the monomial A y^ B.

Kept in this foundational module so direct importers of PFunctor.Basic or PFunctor.Lens.Basic continue to elaborate while migrating to y^.

@[reducible]

def PFunctor.C (A : Type uA) : PFunctor.{uA, uB}

The constant polynomial functor A y^ PEmpty

def PFunctor.linear (A : Type uA) : PFunctor.{uA, uB}

The linear polynomial functor A y^ PUnit

@[reducible]

def PFunctor.selfMonomial (S : Type uA) : PFunctor.{uA, uA}

The self monomial polynomial functor S y^ S.

The body spells out the monomial rather than using S y^ S so that the head and child types are projections of an explicit structure literal at every transparency level; the mate-object equations in the dynamical layers rewrite through this carrier during implicit-transparency checks.

def PFunctor.purePower (B : Type uB) : PFunctor.{uA, uB}

The pure power polynomial functor y^ B, the representable on the type B.

def PFunctor.representable (B : Type uB) : PFunctor.{uA, uB}

A polynomial functor is representable if it is equivalent to y^ A for some type A.

def PFunctor.«termY^_» : Lean.ParserDescr

The pure power polynomial functor y^ B, the representable on the type B.

@[reducible]

def PFunctor.univ : PFunctor.{u + 1, u}

The universe polynomial functor Σ (T : Type u), y^ T: positions are types, and the directions at a position T are its elements. Its extension univ.Obj S is Σ (T : Type u), T → S, so a dynamical system over univ is a transition system that exposes at each state the type of its currently enabled events; see PFunctor.DynSystem.

Reducible so that a direction type univ.B T unfolds to T during elaboration and instance search, keeping transitions over univ as ergonomic as bare functions.

instance PFunctor.instIsEmptyBOfNat_polyFun {a : A 1} : IsEmpty (B 1 a)

instance PFunctor.instIsEmptyBC {α : Type u_1} (a : α) : IsEmpty ((C α).B a)

@[instance_reducible]

instance PFunctor.instUniqueBY {a : y.A} : Unique (y.B a)

@[instance_reducible]

instance PFunctor.instUniqueBLinear {α : Type u_1} (a : α) : Unique ((linear α).B a)

@[instance_reducible]

instance PFunctor.instUniqueAPurePower {β : Type u_1} : Unique (purePower β).A

@[simp]

theorem PFunctor.C_empty : C PEmpty.{u_2 + 1} = 0

@[simp]

theorem PFunctor.C_unit : C PUnit.{u_2 + 1} = 1

@[simp]

theorem PFunctor.C_A (A : Type u) : (C A).A = A

@[simp]

theorem PFunctor.C_B (A : Type u) (a : (C A).A) : (C A).B a = PEmpty.{u_1 + 1}

@[simp]

theorem PFunctor.y_A : y.A = PUnit.{u_1 + 1}

@[simp]

theorem PFunctor.y_B (a : y.A) : y.B a = PUnit.{u_2 + 1}

@[deprecated PFunctor.y_A (since := "2026-08-17")]

theorem PFunctor.X_A : y.A = PUnit.{u_1 + 1}

Alias of PFunctor.y_A.

@[deprecated PFunctor.y_B (since := "2026-08-17")]

theorem PFunctor.X_B (a : y.A) : y.B a = PUnit.{u_2 + 1}

Alias of PFunctor.y_B.

@[simp]

theorem PFunctor.linear_A (A : Type u) : (linear A).A = A

@[simp]

theorem PFunctor.linear_B (A : Type u) (a : (linear A).A) : (linear A).B a = PUnit.{u_1 + 1}

@[simp]

theorem PFunctor.selfMonomial_A (S : Type u) : (selfMonomial S).A = S

@[simp]

theorem PFunctor.selfMonomial_B (S : Type u) (a : (selfMonomial S).A) : (selfMonomial S).B a = S

@[simp]

theorem PFunctor.selfMonomial_unit : selfMonomial PUnit.{u_1 + 1} = y

@[simp]

theorem PFunctor.purePower_A (B : Type u) : (purePower B).A = PUnit.{u_1 + 1}

@[simp]

theorem PFunctor.purePower_B (B : Type u) (a : (purePower B).A) : (purePower B).B a = B

@[simp]

theorem PFunctor.purePower_unit : purePower PUnit.{u_1 + 1} = y

@[simp]

theorem PFunctor.univ_A : univ.A = Type u

theorem PFunctor.univ_B (T : Type u) : univ.B T = T

@[reducible, inline]

abbrev PFunctor.sum (P : PFunctor.{uA₁, uB}) (Q : PFunctor.{uA₂, uB}) : PFunctor.{max uA₁ uA₂, uB}

The sum (coproduct) of two polynomial functors P and Q, written as P + Q.

Defined as the sum of the head types and the dependent sum recursor for the child types. The recursor is written directly so that nested coproduct directions normalize at implicit transparency.

Note: requires the B universe levels to be the same.

@[simp]

theorem PFunctor.sum_A (P : PFunctor.{uA₁, uB}) (Q : PFunctor.{uA₂, uB}) : (P.sum Q).A = (P.A ⊕ Q.A)

@[simp]

theorem PFunctor.sum_B_inl (P : PFunctor.{uA₁, uB}) (Q : PFunctor.{uA₂, uB}) (a : P.A) : (P.sum Q).B (Sum.inl a) = P.B a

@[simp]

theorem PFunctor.sum_B_inr (P : PFunctor.{uA₁, uB}) (Q : PFunctor.{uA₂, uB}) (a : Q.A) : (P.sum Q).B (Sum.inr a) = Q.B a

@[reducible]

instance PFunctor.instHAddPFunctor : HAdd PFunctor.{uA₁, uB} PFunctor.{uA₂, uB} PFunctor.{max uA₁ uA₂, uB}

Addition of polynomial functors, defined as the sum construction.

@[reducible]

instance PFunctor.instAddPFunctor : Add PFunctor.{uA, uB}

theorem PFunctor.add_def (P : PFunctor.{uA₁, uB}) (Q : PFunctor.{uA₂, uB}) : P + Q = { A := P.A ⊕ Q.A, B := Sum.rec P.B Q.B }

def PFunctor.coprod (P : PFunctor.{uA₁, uB}) (Q : PFunctor.{uA₂, uB}) : PFunctor.{max uA₁ uA₂, uB}

Alias of PFunctor.sum.

---

The sum (coproduct) of two polynomial functors P and Q, written as P + Q.

Defined as the sum of the head types and the dependent sum recursor for the child types. The recursor is written directly so that nested coproduct directions normalize at implicit transparency.

Note: requires the B universe levels to be the same.

def PFunctor.sigma {I : Type v} (F : I → PFunctor.{uA, uB}) : PFunctor.{max uA v, uB}

The generalized sum (sigma type) of an indexed family of polynomial functors.

def PFunctor.«termΣₚ_,_» : Lean.ParserDescr

Σₚ i, F i is the indexed sum PFunctor.sigma F of a family of polynomial functors.

def PFunctor.prod (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) : PFunctor.{max uA₁ uA₂, max uB₁ uB₂}

The product of two polynomial functors P and Q, written as P * Q.

Defined as the product of the head types and the sum of the child types.

@[instance_reducible]

instance PFunctor.instHMulPFunctor : HMul PFunctor.{uA₁, uB₁} PFunctor.{uA₂, uB₂} PFunctor.{max uA₁ uA₂, max uB₁ uB₂}

Multiplication of polynomial functors, defined as the product construction.

@[instance_reducible]

instance PFunctor.instMulPFunctor : Mul PFunctor.{uA, uB}

def PFunctor.pi {I : Type v} (F : I → PFunctor.{uA, uB}) : PFunctor.{max uA v, max uB v}

The generalized product (pi type) of an indexed family of polynomial functors.

def PFunctor.«termΠₚ_,_» : Lean.ParserDescr

Πₚ i, F i is the indexed product PFunctor.pi F of a family of polynomial functors.

def PFunctor.tensor (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) : PFunctor.{max uA₁ uA₂, max uB₁ uB₂}

The tensor (also called parallel or Dirichlet) product of two polynomial functors P and Q.

Defined as the product of the head types and the product of the child types.

def PFunctor.«term_⊗_» : Lean.TrailingParserDescr

Infix notation for tensor product P ⊗ Q

def PFunctor.tensorUnit : PFunctor.{uA, uB}

The unit for the tensor product, the variable y

def PFunctor.«term_◃_» : Lean.TrailingParserDescr

Infix notation for PFunctor.comp P Q

def PFunctor.compUnit : PFunctor.{uA, uB}

The unit for composition, the variable y

def PFunctor.compNth (P : PFunctor.{uA, uB}) : ℕ → PFunctor.{max uA uB, uB}

The composition power P ◃^ n, the n-fold composite P ◃ P ◃ ... ◃ P.

def PFunctor.«term_◃^_» : Lean.TrailingParserDescr

The composition power P ◃^ n, the n-fold composite P ◃ P ◃ ... ◃ P.

@[instance_reducible]

instance PFunctor.instNatPowPFunctor : NatPow PFunctor.{max uA uB, uB}

Compatibility instance for the former p ^ n composition-power spelling. The canonical notation is p ◃^ n.

def PFunctor.ulift (P : PFunctor.{uA, uB}) : PFunctor.{max uA vA, max uB vB}

Lift a polynomial functor P to a pair of larger universes.

def PFunctor.exp (P Q : PFunctor.{uA, uB}) : PFunctor.{max uA uB, max uA uB}

Exponential of polynomial functors P ^ Q

@[instance_reducible]

instance PFunctor.instHPowPFunctor : HPow PFunctor.{uA, uB} PFunctor.{uA, uB} PFunctor.{max uA uB, max uA uB}

class PFunctor.Fintype (P : PFunctor.{uA, uB}) : Type (max uA uB)

A polynomial functor is finitely branching if each of its branches is a finite type.

• fintypeB (a : P.A) : Fintype (P.B a)

  The direction type over each position a is a finite type.

@[instance_reducible]

instance PFunctor.instFintypeUlift {P : PFunctor.{uA, uB}} [inst : P.Fintype] : P.ulift.Fintype

@[instance_reducible]

instance PFunctor.instFintypeBOfFintype {P : PFunctor.{uA, uB}} [inst : P.Fintype] (a : P.A) : Fintype (P.B a)

@[instance_reducible]

instance PFunctor.instFintypeOfNat : PFunctor.Fintype 0

@[instance_reducible]

instance PFunctor.instFintypeOfNat_1 : PFunctor.Fintype 1

class PFunctor.Inhabited (P : PFunctor.{uA, uB}) : Type (max uA uB)

A polynomial functor is pointwise inhabited if each of its branches is an inhabited type.

• inhabitedB (a : P.A) : Inhabited (P.B a)

  The direction type over each position a is inhabited.

@[instance_reducible]

instance PFunctor.instInhabitedUlift {P : PFunctor.{uA, uB}} [inst : P.Inhabited] : P.ulift.Inhabited

@[instance_reducible]

instance PFunctor.instInhabitedBOfInhabited {P : PFunctor.{uA, uB}} [inst : P.Inhabited] (a : P.A) : Inhabited (P.B a)

class PFunctor.DecidableEq (P : PFunctor.{uA, uB}) : Type (max uA uB)

A polynomial functor has decidable equality if its position type and each of its direction types have decidable equality.

• decidableEqA : DecidableEq P.A

  The position type P.A has decidable equality.

• decidableEqB (a : P.A) : DecidableEq (P.B a)

  The direction type over each position a has decidable equality.

@[instance_reducible]

instance PFunctor.instDecidableEqAOfDecidableEq {P : PFunctor.{uA, uB}} [inst : P.DecidableEq] : DecidableEq P.A

@[instance_reducible]

instance PFunctor.instDecidableEqBOfDecidableEq {P : PFunctor.{uA, uB}} [inst : P.DecidableEq] (a : P.A) : DecidableEq (P.B a)

@[instance_reducible]

instance PFunctor.instDecidableEqUlift {P : PFunctor.{uA, uB}} [inst : P.DecidableEq] : P.ulift.DecidableEq

@[instance_reducible]

instance PFunctor.instDecidableEqOfNat : PFunctor.DecidableEq 0

@[instance_reducible]

instance PFunctor.instDecidableEqOfNat_1 : PFunctor.DecidableEq 1

def PFunctor.ofConst (A : Type uA) (B : Type uB) : PFunctor.{uA, uB}

PFunctor where the output type is constant over an arbitrary input type.

@[instance_reducible]

instance PFunctor.instFintypeOfConstOfFintype (A : Type uA) (B : Type uB) [hB : Fintype B] : (ofConst A B).Fintype

@[instance_reducible]

instance PFunctor.instDecidableEqOfConstOfDecidableEq (A : Type uA) (B : Type uB) [DecidableEq A] [DecidableEq B] : (ofConst A B).DecidableEq

@[instance_reducible]

instance PFunctor.instInhabitedOfConstOfInhabited (A : Type uA) (B : Type uB) [Inhabited B] : (ofConst A B).Inhabited

structure PFunctor.Equiv (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) : Type (max (max (max uA₁ uA₂) uB₁) uB₂)

An equivalence between two polynomial functors P and Q, written P ≃ₚ Q, is given by an equivalence of the A types and an equivalence between the B types for each a : A.

• equivA : P.A ≃ Q.A

  An equivalence between the A types

• equivB (a : P.A) : P.B a ≃ Q.B (self.equivA a)

  An equivalence between the B types for each a : A

theorem PFunctor.Equiv.ext {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {x y : P.Equiv Q} (equivA : x.equivA = y.equivA) (equivB : x.equivB ≍ y.equivB) : x = y

theorem PFunctor.Equiv.ext_iff {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {x y : P.Equiv Q} : x = y ↔ x.equivA = y.equivA ∧ x.equivB ≍ y.equivB

def PFunctor.«term_≃ₚ_» : Lean.TrailingParserDescr

An equivalence between two polynomial functors P and Q, written P ≃ₚ Q, is given by an equivalence of the A types and an equivalence between the B types for each a : A.

def PFunctor.Equiv.refl (P : PFunctor.{uA, uB}) : P.Equiv P

The identity equivalence between a polynomial functor P and itself.

def PFunctor.Equiv.symm {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} (E : P.Equiv Q) : Q.Equiv P

The inverse of an equivalence between polynomial functors.

def PFunctor.Equiv.trans {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}} (E : P.Equiv Q) (F : Q.Equiv R) : P.Equiv R

The composition of two equivalences between polynomial functors.

def PFunctor.Equiv.cast {P Q : PFunctor.{uA, uB}} (hA : P.A = Q.A) (hB : ∀ (a : P.A), P.B a = Q.B (_root_.cast hA a)) : P.Equiv Q

Equivalence between two polynomial functors P and Q that are equal.

@[simp]

theorem PFunctor.Equiv.symm_comp_self {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} (e : P.Equiv Q) : ⇑e.symm.equivA ∘ ⇑e.equivA = id

theorem PFunctor.Equiv.eqRec_id_apply {α : Sort u} {β : α → Sort v} {a1 a0 : α} (h : a1 = a0) (x : β a0) : Eq.rec (motive := fun (y : α) (x : a1 = y) => β y → β a1) id h x = _root_.cast ⋯ x

Rewrite a dependent Eq.rec with identity to a cast on the argument.

theorem PFunctor.Equiv.equivB_symm_apply_of_eq {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} (e : P.Equiv Q) {a a' : P.A} (ha : e.equivA a = e.equivA a') (b : P.B a') : (e.equivB a).symm ((_root_.Equiv.cast ⋯).symm ((e.equivB a') b)) = _root_.cast ⋯ b

Cast-normalization helper for equivB under equal equivA images.

theorem PFunctor.Equiv.symm_equivB_symm_apply_of_eq {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} (e : P.Equiv Q) {a a' : Q.A} (ha : e.symm.equivA a = e.symm.equivA a') (b : Q.B a') : (e.symm.equivB a).symm ((_root_.Equiv.cast ⋯).symm ((e.symm.equivB a') b)) = _root_.cast ⋯ b

Cast-normalization helper for symm.equivB under equal symm.equivA images.

theorem PFunctor.Equiv.equivB_symm_apply {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} (e : P.Equiv Q) (a : P.A) (b : P.B (e.equivA.symm (e.equivA a))) : (e.equivB a).symm ((e.symm.equivB (e.equivA a)).symm b) = _root_.cast ⋯ b

Specialized cast-normalization for e followed by e.symm.

theorem PFunctor.Equiv.symm_equivB_symm_apply {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} (e : P.Equiv Q) (a : Q.A) (b : Q.B (e.equivA (e.equivA.symm a))) : (e.symm.equivB a).symm ((e.equivB (e.equivA.symm a)).symm b) = _root_.cast ⋯ b

Specialized cast-normalization for e.symm followed by e.

theorem PFunctor.Equiv.forward_equivB_roundtrip {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} (e : P.Equiv Q) (a : P.A) (b : P.B a) : (e.symm.equivB (e.equivA a)) ((e.equivB a) b) = _root_.cast ⋯ b

Forward roundtrip: applying equivB then symm.equivB gives a cast.

theorem PFunctor.Equiv.reverse_equivB_roundtrip {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} (e : P.Equiv Q) (a : Q.A) (b : Q.B a) : (e.equivB (e.equivA.symm a)) ((e.symm.equivB a) b) = _root_.cast ⋯ b

Reverse roundtrip: applying symm.equivB then equivB gives a cast.

structure PFunctor.Lens (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) : Type (max (max (max uA₁ uA₂) uB₁) uB₂)

A lens between two polynomial functors P and Q is a pair of a function:

• toFunA : P.A → Q.A
• toFunB : ∀ a, Q.B (toFunA a) → P.B a

• toFunA : P.A → Q.A

  The forward map on positions, sending each position of P to a position of Q.

• toFunB (a : P.A) : Q.B (self.toFunA a) → P.B a

  The backward map on directions, pulling a direction of Q at toFunA a back to a direction of P at a.

def PFunctor.«term_⇆_» : Lean.TrailingParserDescr

Infix notation for constructing a lens toFunA ⇆ toFunB

structure PFunctor.Chart (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) : Type (max (max (max uA₁ uA₂) uB₁) uB₂)

A chart between two polynomial functors P and Q is a pair of a function:

• toFunA : P.A → Q.A
• toFunB : ∀ a, P.B a → Q.B (toFunA a)

• toFunA : P.A → Q.A

  The forward map on positions, sending each position of P to a position of Q.

• toFunB (a : P.A) : P.B a → Q.B (self.toFunA a)

  The forward map on directions, pushing a direction of P at a to a direction of Q at toFunA a.

def PFunctor.«term_⇉_» : Lean.TrailingParserDescr

Infix notation for constructing a chart toFunA ⇉ toFunB

theorem PFunctor.ext {P Q : PFunctor.{uA, uB}} (h : P.A = Q.A) (h' : ∀ (a : P.A), P.B a = Q.B (h ▸ a)) : P = Q

theorem PFunctor.y_eq_linear_pUnit : y = linear PUnit.{u_2 + 1}

theorem PFunctor.y_eq_purePower_pUnit : y = purePower PUnit.{u_1 + 1}

@[deprecated PFunctor.y_eq_linear_pUnit (since := "2026-08-17")]

theorem PFunctor.X_eq_linear_pUnit : y = linear PUnit.{u_2 + 1}

Alias of PFunctor.y_eq_linear_pUnit.

@[deprecated PFunctor.y_eq_purePower_pUnit (since := "2026-08-17")]

theorem PFunctor.X_eq_purePower_pUnit : y = purePower PUnit.{u_1 + 1}

Alias of PFunctor.y_eq_purePower_pUnit.

@[simp]

theorem PFunctor.ulift_A {P : PFunctor.{uA, uB}} : P.ulift.A = ULift.{u_1, uA} P.A

@[simp]

theorem PFunctor.ulift_B {P : PFunctor.{uA, uB}} {a : P.A} : P.ulift.B { down := a } = ULift.{u_1, uB} (P.B a)