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 PFunctor.instZero_toMathlib : 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)

Equations

• PFunctor.instZero_toMathlib = { zero := { A := PEmpty.{?u.4 + 1}, B := fun (x : PEmpty.{?u.4 + 1}) => PEmpty.{?u.3 + 1} } }

instance PFunctor.instOne_toMathlib : 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)

Equations

• PFunctor.instOne_toMathlib = { one := { A := PUnit.{?u.4 + 1}, B := fun (x : PUnit.{?u.4 + 1}) => PEmpty.{?u.3 + 1} } }

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

The variable y polynomial functor. This is the unit for composition.

Equations

• PFunctor.y = { A := PUnit.{?u.4 + 1}, B := fun (x : PUnit.{?u.4 + 1}) => PUnit.{?u.3 + 1} }

instance PFunctor.instIsEmptyAOfNat_toMathlib : IsEmpty (A 0)

instance PFunctor.instUniqueAOfNat_toMathlib : Unique (A 1)

Equations

• PFunctor.instUniqueAOfNat_toMathlib = inferInstanceAs (Unique PUnit.{?u.3 + 1})

instance PFunctor.instUniqueAY : Unique y.A

Equations

• PFunctor.instUniqueAY = inferInstanceAs (Unique PUnit.{?u.3 + 1})

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

The monomial functor, also written P(X) = A X^ B, has A as its head type and the constant family B_a = B as the child type for each each shape a : A .

Equations

• PFunctor.monomial A B = { A := A, B := fun (x : A) => B }

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

The monomial functor, also written P(X) = A X^ B, has A as its head type and the constant family B_a = B as the child type for each each shape a : A .

Equations

• PFunctor.«term_X^_» = Lean.ParserDescr.trailingNode `PFunctor.«term_X^_» 80 81 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " X^ ") (Lean.ParserDescr.cat `term 80))

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

The constant polynomial functor P(X) = A X^ PEmpty

Equations

• PFunctor.C A = PFunctor.monomial A PEmpty.{?u.6 + 1}

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

The variable (or indeterminate) polynomial functor X, defined as P(X) = PUnit X^ PUnit.

This is the identity with respect to tensor product and composition (up to equivalence).

Equations

• PFunctor.X = PFunctor.monomial PUnit.{?u.3 + 1} PUnit.{?u.2 + 1}

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

The linear polynomial functor P(X) = A X

Equations

• PFunctor.linear A = PFunctor.monomial A PUnit.{?u.6 + 1}

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

The self monomial polynomial functor P(X) = S X^ S

Equations

• PFunctor.selfMonomial S = PFunctor.monomial S S

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

The pure power polynomial functor P(X) = X^ B

Equations

• PFunctor.purePower B = PFunctor.monomial PUnit.{?u.7 + 1} B

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

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

Equations

• PFunctor.representable = PFunctor.purePower

def PFunctor.ofFn {A : Type uA₁} (B : A → Type uB) : PFunctor.{uA₁, uB}

Construct a polynomial functor from just a function B, with A derived implicitly.

Equations

• PFunctor.ofFn B = { A := A, B := B }

@[simp]

theorem PFunctor.ofFn_A {A : Type uA₁} (B : A → Type uB) : (ofFn B).A = A

@[simp]

theorem PFunctor.ofFn_B {A : Type uA₁} (B : A → Type uB) (a : A) : (ofFn B).B a = B a

instance PFunctor.instIsEmptyAOfNat_toMathlib_1 : IsEmpty (A 0)

instance PFunctor.instUniqueAOfNat_toMathlib_1 : Unique (A 1)

Equations

• PFunctor.instUniqueAOfNat_toMathlib_1 = inferInstanceAs (Unique PUnit.{?u.3 + 1})

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

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

instance PFunctor.instUniqueAX : Unique X.A

Equations

• PFunctor.instUniqueAX = inferInstanceAs (Unique PUnit.{?u.3 + 1})

instance PFunctor.instUniqueBX {a : X.A} : Unique (X.B a)

Equations

• PFunctor.instUniqueBX = inferInstanceAs (Unique PUnit.{?u.6 + 1})

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

Equations

• PFunctor.instUniqueBLinear a = inferInstanceAs (Unique PUnit.{?u.11 + 1})

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

Equations

• PFunctor.instUniqueAPurePower = inferInstanceAs (Unique PUnit.{?u.7 + 1})

@[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.X_A : X.A = PUnit.{u_1 + 1}

@[simp]

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

@[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} = X

@[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} = X

def 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 sum case analysis for the child types.

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

Equations

• P.sum Q = { A := P.A ⊕ Q.A, B := Sum.elim P.B Q.B }

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

Addition of polynomial functors, defined as the sum construction.

Equations

• PFunctor.instHAdd_toMathlib = { hAdd := PFunctor.sum }

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

Equations

• PFunctor.instAdd_toMathlib = { add := PFunctor.sum }

theorem PFunctor.add_def (P : PFunctor.{uA₁, uB}) (Q : PFunctor.{uA₂, uB}) : P + Q = { A := P.A ⊕ Q.A, B := Sum.elim 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 sum case analysis for the child types.

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

Equations

• PFunctor.coprod = PFunctor.sum

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.

Equations

• PFunctor.sigma F = { A := (i : I) × (F i).A, B := fun (x : (i : I) × (F i).A) => match x with | ⟨i, a⟩ => (F i).B a }

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.

Equations

• P.prod Q = { A := P.A × Q.A, B := fun (ab : P.A × Q.A) => P.B ab.1 ⊕ Q.B ab.2 }

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

Multiplication of polynomial functors, defined as the product construction.

Equations

• PFunctor.instHMul_toMathlib = { hMul := PFunctor.prod }

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

Equations

• PFunctor.instMul_toMathlib = { mul := PFunctor.prod }

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.

Equations

• PFunctor.pi F = { A := (i : I) → (F i).A, B := fun (f : (i : I) → (F i).A) => (i : I) × (F i).B (f i) }

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.

Equations

• P.tensor Q = { A := P.A × Q.A, B := fun (ab : P.A × Q.A) => P.B ab.1 × Q.B ab.2 }

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

Infix notation for tensor product P ⊗ Q

Equations

• PFunctor.«term_⊗_» = Lean.ParserDescr.trailingNode `PFunctor.«term_⊗_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊗ ") (Lean.ParserDescr.cat `term 71))

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

The unit for the tensor product Y

Equations

• PFunctor.tensorUnit = PFunctor.X

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

Infix notation for PFunctor.comp P Q

Equations

• PFunctor.«term_◃_» = Lean.ParserDescr.trailingNode `PFunctor.«term_◃_» 80 80 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ◃ ") (Lean.ParserDescr.cat `term 81))

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

The unit for composition Y

Equations

• PFunctor.compUnit = PFunctor.X

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

Repeated composition P ◃ P ◃ ... ◃ P (n times).

Equations

• P.compNth 0 = PFunctor.X
• P.compNth n.succ = P.comp (P.compNth n)

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

Equations

• PFunctor.instNatPow_toMathlib = { pow := PFunctor.compNth }

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.

Equations

• P.ulift = { A := ULift.{?u.8, ?u.10} P.A, B := fun (a : ULift.{?u.8, ?u.10} P.A) => ULift.{?u.7, ?u.9} (P.B a.down) }

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

Exponential of polynomial functors P ^ Q

Equations

• P.exp Q = PFunctor.pi fun (a : Q.A) => P.comp (PFunctor.X + PFunctor.C (Q.B a))

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

Equations

• PFunctor.instHPow_toMathlib = { hPow := PFunctor.exp }

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.

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

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

Equations

• PFunctor.instFintypeUlift = { fintype_B := fun (a : P.ulift.A) => id inferInstance }

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

Equations

• PFunctor.instFintypeBOfFintype a = PFunctor.Fintype.fintype_B a

instance PFunctor.instFintypeOfNat : PFunctor.Fintype 0

Equations

• PFunctor.instFintypeOfNat = { fintype_B := fun (x : PFunctor.A 0) => Fintype.instPEmpty }

instance PFunctor.instFintypeOfNat_1 : PFunctor.Fintype 1

Equations

• PFunctor.instFintypeOfNat_1 = { fintype_B := fun (x : PFunctor.A 1) => Fintype.instPEmpty }

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

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

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

Equations

• PFunctor.instInhabitedUlift = { inhabited_B := fun (a : P.ulift.A) => id inferInstance }

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

Equations

• PFunctor.instInhabitedBOfInhabited a = PFunctor.Inhabited.inhabited_B a

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

• decidableEq_A : DecidableEq P.A
• decidableEq_B (a : P.A) : DecidableEq (P.B a)

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

Equations

• PFunctor.instDecidableEqAOfDecidableEq = PFunctor.DecidableEq.decidableEq_A

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

Equations

• PFunctor.instDecidableEqBOfDecidableEq a = PFunctor.DecidableEq.decidableEq_B a

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

Equations

• PFunctor.instDecidableEqUlift = { decidableEq_A := id inferInstance, decidableEq_B := fun (a : P.ulift.A) => id inferInstance }

instance PFunctor.instDecidableEqOfNat : PFunctor.DecidableEq 0

Equations

• PFunctor.instDecidableEqOfNat = { decidableEq_A := inferInstanceAs (DecidableEq PEmpty.{?u.5 + 1}), decidableEq_B := fun (x : PFunctor.A 0) => inferInstanceAs (DecidableEq PEmpty.{?u.4 + 1}) }

instance PFunctor.instDecidableEqOfNat_1 : PFunctor.DecidableEq 1

Equations

• PFunctor.instDecidableEqOfNat_1 = { decidableEq_A := inferInstanceAs (DecidableEq PUnit.{?u.5 + 1}), decidableEq_B := fun (x : PFunctor.A 1) => inferInstanceAs (DecidableEq PEmpty.{?u.4 + 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.

Equations

• PFunctor.ofConst A B = { A := A, B := fun (x : A) => B }

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

Equations

• PFunctor.instFintypeOfConstOfFintype A B = { fintype_B := fun (x : (PFunctor.ofConst A B).A) => inferInstanceAs (Fintype B) }

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

Equations

• PFunctor.instDecidableEqOfConstOfDecidableEq A B = { decidableEq_A := inferInstanceAs (DecidableEq A), decidableEq_B := fun (x : (PFunctor.ofConst A B).A) => inferInstanceAs (DecidableEq B) }

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

Equations

• PFunctor.instInhabitedOfConstOfInhabited A B = { inhabited_B := fun (x : (PFunctor.ofConst A B).A) => inferInstanceAs (Inhabited B) }

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.

Equations

• PFunctor.«term_≃ₚ_» = Lean.ParserDescr.trailingNode `PFunctor.«term_≃ₚ_» 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≃ₚ ") (Lean.ParserDescr.cat `term 26))

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

The identity equivalence between a polynomial functor P and itself.

Equations

• PFunctor.Equiv.refl P = { equivA := Equiv.refl P.A, equivB := fun (a : P.A) => Equiv.refl (P.B a) }

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.

Equations

• E.symm = { equivA := E.equivA.symm, equivB := fun (a : Q.A) => (Equiv.cast ⋯).trans (E.equivB (E.equivA.symm a)).symm }

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.

Equations

• E.trans F = { equivA := E.equivA.trans F.equivA, equivB := fun (a : P.A) => (E.equivB a).trans (F.equivB (E.equivA a)) }

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.

Equations

• PFunctor.Equiv.cast hA hB = { equivA := Equiv.cast hA, equivB := fun (a : P.A) => Equiv.cast ⋯ }

@[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.

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
• toFunB (a : P.A) : Q.B (self.toFunA a) → P.B a

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

Infix notation for constructing a lens toFunA ⇆ toFunB

Equations

• PFunctor.«term_⇆_» = Lean.ParserDescr.trailingNode `PFunctor.«term_⇆_» 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⇆ ") (Lean.ParserDescr.cat `term 25))

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
• toFunB (a : P.A) : P.B a → Q.B (self.toFunA a)

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

Infix notation for constructing a chart toFunA ⇉ toFunB

Equations

• PFunctor.«term_⇉_» = Lean.ParserDescr.trailingNode `PFunctor.«term_⇉_» 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⇉ ") (Lean.ParserDescr.cat `term 25))

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.X_eq_linear_pUnit : X = linear PUnit.{u_2 + 1}

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

@[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)