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₂

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

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

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.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)

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 X)

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

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

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

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

Lens from P ◃ X to P

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

Lens from X ◃ 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 X

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

Helper lens for 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₃}} {X : PFunctor.{uA₅, uB₅}} (l₁ : P.Lens R) (l₂ : Q.Lens W) (f : R.Lens X) (g : W.Lens X) : [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₄}} {X : PFunctor.{uA₅, uB₅}} (l₁ : Q.Lens W) (l₂ : R.Lens X) (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.compX {P : PFunctor.{uA₁, uB₁}} : P.comp X ≃ₗ P

Composition with X is identity (right)

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

Composition with X 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

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

Tensor product with X is identity (right)

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

Tensor product with X 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.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