action of polynomial functor on equiv

Stream: Is there code for X?

[Aaron Liu]

It's useful to know that P.map e and P.map e.symm are inverses, so this seems like the simplest way to encode that

import Mathlib

def PFunctor.mapEquiv {α : Type v} {β : Type w}
    (P : PFunctor.{uA, uB}) (e : α ≃ β) : P α ≃ P β where
  toFun := P.map e
  invFun := P.map e.symm
  left_inv _ := by simp
  right_inv _ := by simp