PFunctor.map_eq_map
theorem PFunctor.map_eq_map : ∀ (P : PFunctor.{u}) {α β : Type v} (f : α → β) (x : ↑P α), f <$> x = P.map f x := by
sorry
This theorem, named `PFunctor.map_eq_map`, demonstrates that for any polynomial functor `P`, a function `f` of type `α → β`, and an object `x` of type `P α`, applying `f` to `x` using the `<$>` operator (also known as the fmap operation in functional programming) is equivalent to directly using the `P.map` operation with `f` and `x`. The comment suggests that the `PFunctor.map` operation is preferred over the `Functor.map` operation because the former is universe-polymorphic, meaning it can operate over objects from any type universe.
More concisely: For any polynomial functor `P`, function `f`, and object `x` of type `P α`, `f <$> x` is equal to `P.map f x`.
|
PFunctor.W.dest_mk
theorem PFunctor.W.dest_mk : ∀ {P : PFunctor.{u}} (p : ↑P P.W), (PFunctor.W.mk p).dest = p
The theorem `PFunctor.W.dest_mk` states that for any polynomial functor `P`, and for any `p` which is a member of type `P` applied to the type `PFunctor.W P`, constructing a W-type from `p` using `PFunctor.W.mk` and then destructing it with `PFunctor.W.dest` yields `p` back. In other words, the destruction function `PFunctor.W.dest` is the left inverse of the construction function `PFunctor.W.mk` for W-types of a polynomial functor. This theorem ensures that W-type construction and destruction operations are reversible.
More concisely: For any polynomial functor `P`, the functions `PFunctor.W.mk` and `PFunctor.W.dest` are mutually inverse, i.e., applying `PFunctor.W.dest` to a W-type constructed by `PFunctor.W.mk` from an element `p` in `P (PFunctor.W P)` yields `p` back.
|
PFunctor.map_eq
theorem PFunctor.map_eq :
∀ (P : PFunctor.{u}) {α : Type v₁} {β : Type v₂} (f : α → β) (a : P.A) (g : P.B a → α),
P.map f ⟨a, g⟩ = ⟨a, f ∘ g⟩
The theorem `PFunctor.map_eq` states that for any PFunctor `P`, for types `α` and `β`, and for any function `f` from `α` to `β`, `a` from the object set of `P` and `g` from the morphism set of `P` to `α`, the application of the `PFunctor.map` operation to these parameters will result in a pair whose first element is `a` and whose second element is the composition of `f` and `g`. In other words, `PFunctor.map` applies the function `f` to the second element of the pair produced by `g`, while leaving the first element `a` unchanged.
More concisely: For any PFunctor `P`, any function `f: α → β`, any object `a` in `P α`, and any morphism `g: β → α` in `P`, `PFunctor.map f g (a, x) = (a, f x)`.
|