Equality of polynomial objects

Extensionality and constructor injectivity through the public shape and child projections of PFunctor.Obj.

theorem PFunctor.Obj.ext {P : PFunctor.{uA, uB}} {α : Type u} {x y : ↑P α} (h : x.fst = y.fst) (h' : x.snd ≍ y.snd) : x = y

Polynomial objects are equal when their shapes and child families agree.

theorem PFunctor.Obj.ext_iff {P : PFunctor.{uA, uB}} {α : Type u} {x y : ↑P α} : x = y ↔ x.fst = y.fst ∧ x.snd ≍ y.snd

theorem PFunctor.Obj.mk.inj {P : PFunctor.{uA, uB}} {α : Type u} {a b : P.A} {f : P.B a → α} {g : P.B b → α} (h : mk a f = mk b g) : a = b ∧ f ≍ g

Equal constructed polynomial objects have equal shapes and child families.

@[simp]

theorem PFunctor.Obj.mk.inj_iff {P : PFunctor.{uA, uB}} {α : Type u} {a b : P.A} {f : P.B a → α} {g : P.B b → α} : mk a f = mk b g ↔ a = b ∧ f ≍ g

Constructor injectivity for polynomial objects.