Commit 2023-11-02 15:26 6668fecb

refactor: use PFunctor.map instead of Functor.map (#7743) Functor.map is monomorphic, so the universe of α in this theorem is fixed to the universe of P:

theorem dest_corec {P : PFunctor.{u}} {α : Type u} (g : α → P α) (x : α) : M.dest (M.corec g x) = M.corec g <$> g x

PFunctor.map is polymorphic, so the universe of α is free from the universe of P:

theorem dest_corec {P : PFunctor.{u}} {α : Type v} (g : α → P α) (x : α) : M.dest (M.corec g x) = P.map (M.corec g) (g x)