More properties about lenses between polynomial functors

theorem heq_forall_iff {α : Sort u} {β γ : α → Sort v} (h : ∀ (a : α), β a = γ a) {f : (a : α) → β a} {g : (a : α) → γ a} : f ≍ g ↔ ∀ (a : α), f a ≍ g a

theorem PFunctor.Lens.ext {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} (l₁ l₂ : P.Lens Q) (h₁ : ∀ (a : P.A), l₁.toFunA a = l₂.toFunA a) (h₂ : ∀ (a : P.A), l₁.toFunB a = Eq.rec (motive := fun (x : Q.A) (h : l₂.toFunA a = x) => Q.B x → P.B a) (l₂.toFunB a) ⋯) : l₁ = l₂

theorem PFunctor.Lens.ext_heq {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} (l₁ l₂ : P.Lens Q) (hA : l₁.toFunA = l₂.toFunA) (hB : l₁.toFunB ≍ l₂.toFunB) : l₁ = l₂

Heterogeneous extensionality for lenses: equal position maps and heterogeneously equal direction maps identify two lenses. Useful when the direction families are equal only after rewriting along the position map.

@[reducible]

def PFunctor.Lens.id (P : PFunctor.{uA, uB}) : P.Lens P

The identity lens

def PFunctor.Lens.comp {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}} (l : Q.Lens R) (l' : P.Lens Q) : P.Lens R

Composition of lenses

def PFunctor.Lens.«term_∘ₗ_» : Lean.TrailingParserDescr

Composition of lenses

def PFunctor.Lens.mapObj {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} (l : P.Lens Q) {α : Type v} (x : ↑P α) : ↑Q α

Apply a polynomial lens to an element of the source polynomial's extension. The position is sent forward and the payload is pulled back along the lens's direction map.

@[simp]

theorem PFunctor.Lens.mapObj_id {P : PFunctor.{uA, uB}} {α : Type v} (x : ↑P α) : (Lens.id P).mapObj x = x

@[simp]

theorem PFunctor.Lens.mapObj_comp {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}} (g : Q.Lens R) (f : P.Lens Q) {α : Type v} (x : ↑P α) : (g ∘ₗ f).mapObj x = g.mapObj (f.mapObj x)

theorem PFunctor.Lens.ext_mapObj {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} (l₁ l₂ : P.Lens Q) (h : ∀ (a : P.A), l₁.mapObj (Obj.mk a id) = l₂.mapObj (Obj.mk a id)) : l₁ = l₂

Two lenses are equal when they act equally on every source position equipped with its identity direction labelling. This packages the dependent position equality and direction-map transport needed by Lens.ext.

@[simp]

theorem PFunctor.Lens.id_comp {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} (f : P.Lens Q) : Lens.id Q ∘ₗ f = f

@[simp]

theorem PFunctor.Lens.comp_id {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} (f : P.Lens Q) : f ∘ₗ Lens.id P = f

theorem PFunctor.Lens.comp_assoc {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}} {S : PFunctor.{uA₄, uB₄}} (l : R.Lens S) (l' : Q.Lens R) (l'' : P.Lens Q) : l ∘ₗ l' ∘ₗ l'' = l ∘ₗ (l' ∘ₗ l'')

structure PFunctor.Lens.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, using lenses. This corresponds to an isomorphism in the category PFunctor with Lens morphisms.

• toLens : P.Lens Q

  The forward lens of the equivalence, from P to Q.

• invLens : Q.Lens P

  The backward lens of the equivalence, from Q to P.

• left_inv : self.invLens ∘ₗ self.toLens = Lens.id P
• right_inv : self.toLens ∘ₗ self.invLens = Lens.id Q

theorem PFunctor.Lens.Equiv.ext_iff {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {x y : P ≃ₗ Q} : x = y ↔ x.toLens = y.toLens ∧ x.invLens = y.invLens

theorem PFunctor.Lens.Equiv.ext {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {x y : P ≃ₗ Q} (toLens : x.toLens = y.toLens) (invLens : x.invLens = y.invLens) : x = y

def PFunctor.Lens.«term_≃ₗ_» : Lean.TrailingParserDescr

An equivalence between two polynomial functors P and Q, using lenses. This corresponds to an isomorphism in the category PFunctor with Lens morphisms.

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

The identity equivalence on P, built from the identity lens in both directions.

def PFunctor.Lens.Equiv.symm {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} (e : P ≃ₗ Q) : Q ≃ₗ P

The inverse equivalence, swapping the forward and backward lenses of e.

def PFunctor.Lens.Equiv.trans {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}} (e₁ : P ≃ₗ Q) (e₂ : Q ≃ₗ R) : P ≃ₗ R

The composite equivalence P ≃ₗ R obtained by chaining e₁ : P ≃ₗ Q and e₂ : Q ≃ₗ R.

theorem PFunctor.Lens.cancel_toLens {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}} (e : P ≃ₗ Q) {f g : R.Lens P} (h : e.toLens ∘ₗ f = e.toLens ∘ₗ g) : f = g

Cancel postcomposition with the forward lens of a lens equivalence.

def PFunctor.Lens.initial {P : PFunctor.{uA, uB}} : Lens 0 P

The (unique) initial lens from the zero functor to any functor P.

def PFunctor.Lens.terminal {P : PFunctor.{uA, uB}} : P.Lens 1

The (unique) terminal lens from any functor P to the unit functor 1.

def PFunctor.Lens.fromZero {P : PFunctor.{uA, uB}} : Lens 0 P

Alias of PFunctor.Lens.initial.

---

The (unique) initial lens from the zero functor to any functor P.

def PFunctor.Lens.toOne {P : PFunctor.{uA, uB}} : P.Lens 1

Alias of PFunctor.Lens.terminal.

---

The (unique) terminal lens from any functor P to the unit functor 1.

def PFunctor.Lens.fromY {P : PFunctor.{uA, uB}} (a : P.A) : y.Lens P

Construct a lens from the variable polynomial by selecting a position. The backward map is uniquely determined by the unit direction of y.

@[simp]

theorem PFunctor.Lens.fromY_toFunA {P : PFunctor.{uA, uB}} (a : P.A) (u : PUnit.{uA₁ + 1}) : (fromY a).toFunA u = a

@[simp]

theorem PFunctor.Lens.fromY_toFunB {P : PFunctor.{uA, uB}} (a : P.A) (u : PUnit.{uA₁ + 1}) (d : P.B a) : (fromY a).toFunB u d = PUnit.unit

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

def PFunctor.Lens.fromX {P : PFunctor.{uA, uB}} (a : P.A) : y.Lens P

Alias of PFunctor.Lens.fromY.

---

Construct a lens from the variable polynomial by selecting a position. The backward map is uniquely determined by the unit direction of y.

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

theorem PFunctor.Lens.fromX_toFunA {P : PFunctor.{uA, uB}} (a : P.A) (u : PUnit.{uA₁ + 1}) : (fromY a).toFunA u = a

Alias of PFunctor.Lens.fromY_toFunA.

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

theorem PFunctor.Lens.fromX_toFunB {P : PFunctor.{uA, uB}} (a : P.A) (u : PUnit.{uA₁ + 1}) (d : P.B a) : (fromY a).toFunB u d = PUnit.unit

Alias of PFunctor.Lens.fromY_toFunB.

def PFunctor.Lens.toConst {P : PFunctor.{uA, uB}} {A : Type uA₂} (f : P.A → A) : P.Lens (C A)

Construct a lens into a constant polynomial from its position map. The backward map is uniquely determined by the empty direction type.

@[simp]

theorem PFunctor.Lens.toConst_toFunA {P : PFunctor.{uA, uB}} {A : Type uA₂} (f : P.A → A) (a : P.A) : (toConst f).toFunA a = f a

def PFunctor.Lens.toLinear {P : PFunctor.{uA, uB}} {A : Type uA₂} (f : P.A → A) (choose : (a : P.A) → P.B a) : P.Lens (linear A)

Construct a lens into a linear polynomial from a position map and a choice of source direction over every position.

@[simp]

theorem PFunctor.Lens.toLinear_toFunA {P : PFunctor.{uA, uB}} {A : Type uA₂} (f : P.A → A) (choose : (a : P.A) → P.B a) (a : P.A) : (toLinear f choose).toFunA a = f a

@[simp]

theorem PFunctor.Lens.toLinear_toFunB {P : PFunctor.{uA, uB}} {A : Type uA₂} (f : P.A → A) (choose : (a : P.A) → P.B a) (a : P.A) (u : PUnit.{uB₁ + 1}) : (toLinear f choose).toFunB a u = choose a

def PFunctor.Lens.inl {P : PFunctor.{uA₁, uB}} {Q : PFunctor.{uA₂, uB}} : P.Lens (P + Q)

Left injection lens inl : P → P + Q

def PFunctor.Lens.inr {P : PFunctor.{uA₁, uB}} {Q : PFunctor.{uA₂, uB}} : Q.Lens (P + Q)

Right injection lens inr : Q → P + Q

def PFunctor.Lens.sumPair {P : PFunctor.{uA₁, uB}} {Q : PFunctor.{uA₂, uB}} {R : PFunctor.{uA₃, uB₃}} (l₁ : P.Lens R) (l₂ : Q.Lens R) : (P + Q).Lens R

Copairing of lenses [l₁, l₂]ₗ : P + Q → R

def PFunctor.Lens.sumMap {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₁}} {R : PFunctor.{uA₃, uB₃}} {W : PFunctor.{uA₄, uB₃}} (l₁ : P.Lens R) (l₂ : Q.Lens W) : (P + Q).Lens (R + W)

Parallel application of lenses for coproduct l₁ ⊎ l₂ : P + Q → R + W

def PFunctor.Lens.sigmaExists {I : Type v} {F : I → PFunctor.{uA₁, uB₁}} {R : PFunctor.{uA₂, uB₂}} (l : (i : I) → (F i).Lens R) : (sigma F).Lens R

Dependent copairing of lenses over sigma: Σ i, F i → R.

def PFunctor.Lens.sigmaMap {I : Type v} {F : I → PFunctor.{uA₁, uB₁}} {G : I → PFunctor.{uA₂, uB₂}} (l : (i : I) → (F i).Lens (G i)) : (sigma F).Lens (sigma G)

Pointwise mapping of lenses over sigma.

def PFunctor.Lens.fst {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} : (P * Q).Lens P

Projection lens fst : P * Q → P

def PFunctor.Lens.snd {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} : (P * Q).Lens Q

Projection lens snd : P * Q → Q

def PFunctor.Lens.prodPair {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}} (l₁ : P.Lens Q) (l₂ : P.Lens R) : P.Lens (Q * R)

Pairing of lenses ⟨l₁, l₂⟩ₗ : P → Q * R

def PFunctor.Lens.prodMap {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}} {W : PFunctor.{uA₄, uB₄}} (l₁ : P.Lens R) (l₂ : Q.Lens W) : (P * Q).Lens (R * W)

Parallel application of lenses for product l₁ ×ₗ l₂ : P * Q → R * W

def PFunctor.Lens.piForall {I : Type v} {P : PFunctor.{uA₁, uB₁}} {F : I → PFunctor.{uA₂, uB₂}} (l : (i : I) → P.Lens (F i)) : P.Lens (pi F)

Dependent pairing of lenses into a pi: P → ∀ i, F i.

def PFunctor.Lens.piMap {I : Type v} {F : I → PFunctor.{uA₁, uB₁}} {G : I → PFunctor.{uA₂, uB₂}} (l : (i : I) → (F i).Lens (G i)) : (pi F).Lens (pi G)

Pointwise mapping of lenses over pi.

def PFunctor.Lens.compMap {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}} {W : PFunctor.{uA₄, uB₄}} (l₁ : P.Lens R) (l₂ : Q.Lens W) : (P.comp Q).Lens (R.comp W)

Apply lenses to both sides of a composition: l₁ ◃ₗ l₂ : (P ◃ Q ⇆ R ◃ W)

@[implicit_reducible]

def PFunctor.Lens.tensorMap {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}} {W : PFunctor.{uA₄, uB₄}} (l₁ : P.Lens R) (l₂ : Q.Lens W) : (P.tensor Q).Lens (R.tensor W)

Apply lenses to both sides of a tensor / parallel product: l₁ ⊗ₗ l₂ : (P ⊗ Q ⇆ R ⊗ W)

def PFunctor.Lens.tildeR {P : PFunctor.{uA, uB}} : P.Lens (P.comp y)

Lens to introduce y on the right: P → P ◃ y

def PFunctor.Lens.tildeL {P : PFunctor.{uA, uB}} : P.Lens (y.comp P)

Lens to introduce y on the left: P → y ◃ P

def PFunctor.Lens.invTildeR {P : PFunctor.{uA, uB}} : (P.comp y).Lens P

Lens from P ◃ y to P

def PFunctor.Lens.invTildeL {P : PFunctor.{uA, uB}} : (y.comp P).Lens P

Lens from y ◃ P to P

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

Apply lenses to both sides of a composition: l₁ ◃ₗ l₂ : (P ◃ Q ⇆ R ◃ W)

def PFunctor.Lens.«term_×ₗ_» : Lean.TrailingParserDescr

Parallel application of lenses for product l₁ ×ₗ l₂ : P * Q → R * W

def PFunctor.Lens.«term_⊎ₗ_» : Lean.TrailingParserDescr

Parallel application of lenses for coproduct l₁ ⊎ l₂ : P + Q → R + W

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

Apply lenses to both sides of a tensor / parallel product: l₁ ⊗ₗ l₂ : (P ⊗ Q ⇆ R ⊗ W)

def PFunctor.Lens.«term[_,_]ₗ» : Lean.ParserDescr

Notation for the copairing sumPair l₁ l₂ of two lenses out of a sum.

def PFunctor.Lens.«term⟨_,_⟩ₗ» : Lean.ParserDescr

Notation for the pairing prodPair l₁ l₂ of two lenses into a product.

def PFunctor.Lens.enclose (P : PFunctor.{uA, uB}) : Type (max uA uA₁ uB uB₁)

The type of lenses from a polynomial functor P to y

def PFunctor.Lens.fixState {S : Type u} : (selfMonomial S).Lens ((selfMonomial S).comp (selfMonomial S))

The transition lens δ : Sy^S ⇆ Sy^S ◃ Sy^S on the self-monomial state polynomial (Spivak–Niu Example 6.44): δ = (id, tgt, run) remembers the start state, relabels each direction by the state it targets, and composes two hops into one. It is the comultiplication of the state comonoid stateComonoid S, and the helper behind speedup.

def PFunctor.Lens.speedup {S : Type u} {P : PFunctor.{uA, uB}} (l : (selfMonomial S).Lens P) : (selfMonomial S).Lens (P.comp P)

The speedup lens operation: Lens (S y^S) P → Lens (S y^S) (P ◃ P)

@[simp]

theorem PFunctor.Lens.sumMap_comp_inl {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₁}} {R : PFunctor.{uA₃, uB₃}} {W : PFunctor.{uA₄, uB₃}} (l₁ : P.Lens R) (l₂ : Q.Lens W) : l₁ ⊎ₗ l₂ ∘ₗ inl = inl ∘ₗ l₁

@[simp]

theorem PFunctor.Lens.sumMap_comp_inr {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₁}} {R : PFunctor.{uA₃, uB₃}} {W : PFunctor.{uA₄, uB₃}} (l₁ : P.Lens R) (l₂ : Q.Lens W) : l₁ ⊎ₗ l₂ ∘ₗ inr = inr ∘ₗ l₂

theorem PFunctor.Lens.sumPair_comp_sumMap {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₁}} {R : PFunctor.{uA₃, uB₃}} {W : PFunctor.{uA₄, uB₃}} {V : PFunctor.{uA₅, uB₅}} (l₁ : P.Lens R) (l₂ : Q.Lens W) (f : R.Lens V) (g : W.Lens V) : [f,g]ₗ ∘ₗ (l₁ ⊎ₗ l₂) = [f ∘ₗ l₁,g ∘ₗ l₂]ₗ

@[simp]

theorem PFunctor.Lens.sumPair_comp_inl {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₁}} {R : PFunctor.{uA₃, uB₃}} (f : P.Lens R) (g : Q.Lens R) : [f,g]ₗ ∘ₗ inl = f

@[simp]

theorem PFunctor.Lens.sumPair_comp_inr {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₁}} {R : PFunctor.{uA₃, uB₃}} (f : P.Lens R) (g : Q.Lens R) : [f,g]ₗ ∘ₗ inr = g

theorem PFunctor.Lens.comp_inl_inr {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₁}} {R : PFunctor.{uA₃, uB₃}} (h : (P + Q).Lens R) : [h ∘ₗ inl,h ∘ₗ inr]ₗ = h

@[simp]

theorem PFunctor.Lens.sumMap_id {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₁}} : Lens.id P ⊎ₗ Lens.id Q = Lens.id (P + Q)

@[simp]

theorem PFunctor.Lens.sumPair_inl_inr {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₁}} : [inl,inr]ₗ = Lens.id (P + Q)

def PFunctor.Lens.Equiv.sumComm (P : PFunctor.{uA₁, uB}) (Q : PFunctor.{uA₂, uB}) : P + Q ≃ₗ Q + P

Commutativity of coproduct

@[simp]

theorem PFunctor.Lens.Equiv.sumComm_symm {P : PFunctor.{uA₁, uB}} {Q : PFunctor.{uA₂, uB}} : (sumComm P Q).symm = sumComm Q P

def PFunctor.Lens.Equiv.sumAssoc {P : PFunctor.{uA₁, uB}} {Q : PFunctor.{uA₂, uB}} {R : PFunctor.{uA₃, uB}} : P + Q + R ≃ₗ P + (Q + R)

Associativity of coproduct

def PFunctor.Lens.Equiv.sumZero {P : PFunctor.{uA₁, uB}} : P + 0 ≃ₗ P

Coproduct with 0 is identity (right)

def PFunctor.Lens.Equiv.zeroCoprod {P : PFunctor.{uA₁, uB}} : 0 + P ≃ₗ P

Coproduct with 0 is identity (left)

@[simp]

theorem PFunctor.Lens.fst_comp_prodMap {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}} {W : PFunctor.{uA₄, uB₄}} (l₁ : P.Lens R) (l₂ : Q.Lens W) : fst ∘ₗ (l₁ ×ₗ l₂) = l₁ ∘ₗ fst

@[simp]

theorem PFunctor.Lens.snd_comp_prodMap {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}} {W : PFunctor.{uA₄, uB₄}} (l₁ : P.Lens R) (l₂ : Q.Lens W) : snd ∘ₗ (l₁ ×ₗ l₂) = l₂ ∘ₗ snd

theorem PFunctor.Lens.prodMap_comp_prodPair {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}} {W : PFunctor.{uA₄, uB₄}} {V : PFunctor.{uA₅, uB₅}} (l₁ : Q.Lens W) (l₂ : R.Lens V) (f : P.Lens Q) (g : P.Lens R) : l₁ ×ₗ l₂ ∘ₗ ⟨f,g⟩ₗ = ⟨l₁ ∘ₗ f,l₂ ∘ₗ g⟩ₗ

@[simp]

theorem PFunctor.Lens.fst_comp_prodPair {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}} (f : P.Lens Q) (g : P.Lens R) : fst ∘ₗ ⟨f,g⟩ₗ = f

@[simp]

theorem PFunctor.Lens.snd_comp_prodPair {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}} (f : P.Lens Q) (g : P.Lens R) : snd ∘ₗ ⟨f,g⟩ₗ = g

theorem PFunctor.Lens.comp_fst_snd {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}} (h : P.Lens (Q * R)) : ⟨fst ∘ₗ h,snd ∘ₗ h⟩ₗ = h

@[simp]

theorem PFunctor.Lens.prodMap_id {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} : Lens.id P ×ₗ Lens.id Q = Lens.id (P * Q)

@[simp]

theorem PFunctor.Lens.prodPair_fst_snd {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} : ⟨fst,snd⟩ₗ = Lens.id (P * Q)

def PFunctor.Lens.Equiv.prodComm (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) : P * Q ≃ₗ Q * P

Commutativity of product

@[simp]

theorem PFunctor.Lens.Equiv.prodComm_symm {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} : (prodComm P Q).symm = prodComm Q P

def PFunctor.Lens.Equiv.prodAssoc {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}} : P * Q * R ≃ₗ P * (Q * R)

Associativity of product

def PFunctor.Lens.Equiv.prodOne {P : PFunctor.{uA₁, uB₁}} : P * 1 ≃ₗ P

Product with 1 is identity (right)

def PFunctor.Lens.Equiv.oneProd {P : PFunctor.{uA₁, uB₁}} : 1 * P ≃ₗ P

Product with 1 is identity (left)

def PFunctor.Lens.Equiv.prodZero {P : PFunctor.{uA₁, uB₁}} : P * 0 ≃ₗ 0

Product with 0 is zero (right)

def PFunctor.Lens.Equiv.zeroProd {P : PFunctor.{uA₁, uB₁}} : 0 * P ≃ₗ 0

Product with 0 is zero (left)

def PFunctor.Lens.Equiv.prodCoprodDistrib {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₂}} : P * (Q + R) ≃ₗ P * Q + P * R

Left distributive law for product over coproduct

def PFunctor.Lens.Equiv.sumProdDistrib {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₂}} : (Q + R) * P ≃ₗ Q * P + R * P

Right distributive law for coproduct over product

@[simp]

theorem PFunctor.Lens.compMap_id {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} : Lens.id P ◃ₗ Lens.id Q = Lens.id (P.comp Q)

theorem PFunctor.Lens.compMap_comp {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}} {P' : PFunctor.{uA₄, uB₄}} {Q' : PFunctor.{uA₅, uB₅}} {R' : PFunctor.{uA₆, uB₆}} (l₁ : P.Lens P') (l₂ : Q.Lens Q') (l₁' : P'.Lens R) (l₂' : Q'.Lens R') : l₁' ∘ₗ l₁ ◃ₗ (l₂' ∘ₗ l₂) = l₁' ◃ₗ l₂' ∘ₗ (l₁ ◃ₗ l₂)

def PFunctor.Lens.Equiv.compAssoc {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}} : (P.comp Q).comp R ≃ₗ P.comp (Q.comp R)

Associativity of composition

def PFunctor.Lens.Equiv.compY {P : PFunctor.{uA₁, uB₁}} : P.comp y ≃ₗ P

Composition with y is identity (right)

def PFunctor.Lens.Equiv.yComp {P : PFunctor.{uA₁, uB₁}} : y.comp P ≃ₗ P

Composition with y is identity (left)

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

def PFunctor.Lens.Equiv.compX {P : PFunctor.{uA₁, uB₁}} : P.comp y ≃ₗ P

Alias of PFunctor.Lens.Equiv.compY.

---

Composition with y is identity (right)

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

def PFunctor.Lens.Equiv.XComp {P : PFunctor.{uA₁, uB₁}} : y.comp P ≃ₗ P

Alias of PFunctor.Lens.Equiv.yComp.

---

Composition with y is identity (left)

def PFunctor.Lens.Equiv.sumCompDistrib {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₂}} : (Q + R).comp P ≃ₗ Q.comp P + R.comp P

Distributivity of composition over coproduct on the right

@[simp]

theorem PFunctor.Lens.tensorMap_id {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} : Lens.id P ⊗ₗ Lens.id Q = Lens.id (P.tensor Q)

theorem PFunctor.Lens.tensorMap_comp {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}} {P' : PFunctor.{uA₄, uB₄}} {Q' : PFunctor.{uA₅, uB₅}} {R' : PFunctor.{uA₆, uB₆}} (l₁ : P.Lens P') (l₂ : Q.Lens Q') (l₁' : P'.Lens R) (l₂' : Q'.Lens R') : l₁' ∘ₗ l₁ ⊗ₗ (l₂' ∘ₗ l₂) = l₁' ⊗ₗ l₂' ∘ₗ (l₁ ⊗ₗ l₂)

def PFunctor.Lens.Equiv.tensorComm (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) : P.tensor Q ≃ₗ Q.tensor P

Commutativity of tensor product

def PFunctor.Lens.Equiv.tensorAssoc {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}} : (P.tensor Q).tensor R ≃ₗ P.tensor (Q.tensor R)

Associativity of tensor product

@[simp]

theorem PFunctor.Lens.Equiv.tensorAssoc_toFunA {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}} (position : ((P.tensor Q).tensor R).A) : tensorAssoc.toLens.toFunA position = (position.1.1, position.1.2, position.2)

@[simp]

theorem PFunctor.Lens.Equiv.tensorAssoc_toFunB {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}} (position : ((P.tensor Q).tensor R).A) (direction : (P.tensor (Q.tensor R)).B (tensorAssoc.toLens.toFunA position)) : tensorAssoc.toLens.toFunB position direction = ((direction.1, direction.2.1), direction.2.2)

def PFunctor.Lens.Equiv.tensorY {P : PFunctor.{uA₁, uB₁}} : P.tensor y ≃ₗ P

Tensor product with y is identity (right)

def PFunctor.Lens.Equiv.yTensor {P : PFunctor.{uA₁, uB₁}} : y.tensor P ≃ₗ P

Tensor product with y is identity (left)

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

def PFunctor.Lens.Equiv.tensorX {P : PFunctor.{uA₁, uB₁}} : P.tensor y ≃ₗ P

Alias of PFunctor.Lens.Equiv.tensorY.

---

Tensor product with y is identity (right)

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

def PFunctor.Lens.Equiv.xTensor {P : PFunctor.{uA₁, uB₁}} : y.tensor P ≃ₗ P

Alias of PFunctor.Lens.Equiv.yTensor.

---

Tensor product with y is identity (left)

def PFunctor.Lens.Equiv.zeroTensor {P : PFunctor.{uA₁, uB₁}} : tensor 0 P ≃ₗ 0

Tensor product with 0 is zero (left)

def PFunctor.Lens.Equiv.tensorZero {P : PFunctor.{uA₁, uB₁}} : P.tensor 0 ≃ₗ 0

Tensor product with 0 is zero (right)

def PFunctor.Lens.Equiv.tensorCoprodDistrib {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₂}} : P.tensor (Q + R) ≃ₗ P.tensor Q + P.tensor R

Left distributivity of tensor product over coproduct

def PFunctor.Lens.Equiv.sumTensorDistrib {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₂}} : (Q + R).tensor P ≃ₗ Q.tensor P + R.tensor P

Right distributivity of tensor product over coproduct

def PFunctor.Lens.unitComparison : y.Lens y

The unique comparison between two possibly differently instantiated copies of the common tensor/composition unit y.

theorem PFunctor.Lens.yTensor_natural {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} (f : P.Lens Q) : f ∘ₗ Equiv.yTensor.toLens = Equiv.yTensor.toLens ∘ₗ (unitComparison ⊗ₗ f)

Naturality of the left tensor unitor. The unit component is the canonical comparison between the independently instantiated source and target copies of y.

theorem PFunctor.Lens.tensorY_natural {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} (f : P.Lens Q) : f ∘ₗ Equiv.tensorY.toLens = Equiv.tensorY.toLens ∘ₗ (f ⊗ₗ unitComparison)

Naturality of the right tensor unitor. The unit component is the canonical comparison between the independently instantiated source and target copies of y.

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

theorem PFunctor.Lens.xTensor_natural {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} (f : P.Lens Q) : f ∘ₗ Equiv.yTensor.toLens = Equiv.yTensor.toLens ∘ₗ (unitComparison ⊗ₗ f)

Alias of PFunctor.Lens.yTensor_natural.

---

Naturality of the left tensor unitor. The unit component is the canonical comparison between the independently instantiated source and target copies of y.

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

theorem PFunctor.Lens.tensorX_natural {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} (f : P.Lens Q) : f ∘ₗ Equiv.tensorY.toLens = Equiv.tensorY.toLens ∘ₗ (f ⊗ₗ unitComparison)

Alias of PFunctor.Lens.tensorY_natural.

---

Naturality of the right tensor unitor. The unit component is the canonical comparison between the independently instantiated source and target copies of y.

theorem PFunctor.Lens.tensorAssoc_natural {P₁ : PFunctor.{uA₁, uB₁}} {P₂ : PFunctor.{uA₂, uB₂}} {Q₁ : PFunctor.{uA₃, uB₃}} {Q₂ : PFunctor.{uA₄, uB₄}} {R₁ : PFunctor.{uA₅, uB₅}} {R₂ : PFunctor.{uA₆, uB₆}} (f : P₁.Lens P₂) (g : Q₁.Lens Q₂) (h : R₁.Lens R₂) : f ⊗ₗ (g ⊗ₗ h) ∘ₗ Equiv.tensorAssoc.toLens = Equiv.tensorAssoc.toLens ∘ₗ (f ⊗ₗ g ⊗ₗ h)

Naturality of the tensor associator across lenses whose source and target polynomials may occupy six independent universe pairs.

def PFunctor.Equiv.toLensEquiv {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} (e : P.Equiv Q) : P ≃ₗ Q

Convert an equivalence between two polynomial functors P and Q to a lens.

instance PFunctor.Lens.instIsEmptyASigma {I : Type v} [IsEmpty I] {F : I → PFunctor.{u, u_1}} : IsEmpty (sigma F).A

instance PFunctor.Lens.instIsEmptyBSigma {I : Type v} [IsEmpty I] {F : I → PFunctor.{u, u_1}} {a : (sigma F).A} : IsEmpty ((sigma F).B a)

def PFunctor.Lens.sigmaEmpty {I : Type v} [IsEmpty I] {F : I → PFunctor.{uA, uB}} : sigma F ≃ₗ 0

Sigma of an empty family is the zero functor.

def PFunctor.Lens.sigmaUnit {F : PUnit.{u_1 + 1} → PFunctor.{uA, uB}} : sigma F ≃ₗ (F PUnit.unit).ulift

Sigma of a PUnit-indexed family is equivalent to the functor itself (up to ulift).

def PFunctor.Lens.sigmaOfUnique {I : Type v} [Unique I] {F : I → PFunctor.{uA, uB}} : sigma F ≃ₗ (F default).ulift

Sigma of a unique-indexed family is equivalent to the default fiber (up to ulift).

def PFunctor.Lens.prodSigmaDistrib {I : Type v} {P : PFunctor.{uA₁, uB₁}} {F : I → PFunctor.{uA₂, uB₂}} : P * sigma F ≃ₗ sigma fun (i : I) => P * F i

Left distributivity of product over sigma.

def PFunctor.Lens.sigmaProdDistrib {I : Type v} {P : PFunctor.{uA₁, uB₁}} {F : I → PFunctor.{uA₂, uB₂}} : sigma F * P ≃ₗ sigma fun (i : I) => F i * P

Right distributivity of product over sigma.

def PFunctor.Lens.tensorSigmaDistrib {I : Type v} {P : PFunctor.{uA₁, uB₁}} {F : I → PFunctor.{uA₂, uB₂}} : P.tensor (sigma F) ≃ₗ sigma fun (i : I) => P.tensor (F i)

Left distributivity of tensor product over sigma.

def PFunctor.Lens.sigmaTensorDistrib {I : Type v} {P : PFunctor.{uA₂, uB₂}} {F : I → PFunctor.{uA₁, uB₁}} : (sigma F).tensor P ≃ₗ sigma fun (i : I) => (F i).tensor P

Right distributivity of tensor product over sigma.

def PFunctor.Lens.sigmaCompDistrib {I : Type v} {P : PFunctor.{uA₂, uB₂}} {F : I → PFunctor.{uA₁, uB₁}} : (sigma F).comp P ≃ₗ sigma fun (i : I) => (F i).comp P

Right distributivity of composition over sigma.

def PFunctor.Lens.piUnit {P : PFunctor.{u, u_1}} : (pi fun (x : PUnit.{u_2 + 1}) => P) ≃ₗ P

Pi over a PUnit-indexed family is equivalent to the functor itself.

def PFunctor.Lens.piZero {I : Type v} [Inhabited I] {F : I → PFunctor.{uA, uB}} (F_zero : ∀ (i : I), F i = 0) : pi F ≃ₗ 0

Pi of a family of zero functors over an inhabited type is the zero functor.

def PFunctor.Lens.Equiv.ulift {P : PFunctor.{uA, uB}} : P.ulift ≃ₗ P

ULift equivalence for lenses